Add ordtriexmidlem2 to iset.mm
Add ordtriexmidlem2 to iset.mm

This factors out a piece of the ordtriexmid proof. Use the lemma
in ordtriexmid and ordsoexmid (which had been proving the same
thing in a different way).

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