Add weak linearity of ordinals to iet.mm
Add weak linearity of ordinals to iet.mm

Add theorem ordsoexmid which shows that weak linearity of ordinals
implies the law of the excluded middle (as trichotomy does).

Split ordtriexmidlem out from the ordtriexmid proof.

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