theorem :: JORDAN21:43

for A, B being Subset of (TOP-REAL 2) st A c= B & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_above holds
(UMP A) `2 <= (UMP B) `2