let A, B be Subset of (TOP-REAL 2); :: thesis: ( 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 implies (UMP A) `2 <= (UMP B) `2 )
assume that
A1: A c= B and
A2: (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) and
A3: not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty and
A4: proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_above ; :: thesis: (UMP A) `2 <= (UMP B) `2
set w = ((W-bound A) + (E-bound A)) / 2;
( not proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is empty & A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) c= B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) ) by A1, A3, Lm1, RELAT_1:119, XBOOLE_1:26;
then upper_bound (proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) <= upper_bound (proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) by A4, RELAT_1:123, SEQ_4:48;
then (UMP A) `2 <= upper_bound (proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) by EUCLID:52;
hence (UMP A) `2 <= (UMP B) `2 by A2, EUCLID:52; :: thesis: verum