Add isoti to iset.mm
Add isoti to iset.mm

Similar to isoso but for the tightness condition which many of the
supremum theorems have.

Includes isotilem which is one direction of the biconditional.

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