Add recgt0 to iset.mm
Add recgt0 to iset.mm

The statement of the theorem is as in set.mm. The proof needs to
have not equal changed to apart (and, relatedly, trichotomy
changed to ltleap ).

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