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_below implies (LMP B) `2 <= (LMP A) `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_below ; :: thesis: (LMP B) `2 <= (LMP A) `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 lower_bound (proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) >= lower_bound (proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) by A4, RELAT_1:123, SEQ_4:47;
then (LMP A) `2 >= lower_bound (proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) by EUCLID:52;
hence (LMP B) `2 <= (LMP A) `2 by A2, EUCLID:52; :: thesis: verum