Remove more trichotomy theorems from iset.mm
Remove more trichotomy theorems from iset.mm

This is issod , issoi , and isso2i . We might want analogues
which use weak linearity instead of trichotomy, but that can
wait until we have a place to use them.

metamath/set.mm,metamath/set.mm,metamath/set.mm