let A, B be Subset of (TOP-REAL 2); :: thesis: ( A c= B & LMP B in A & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_below & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) implies LMP A = LMP B )
assume that
A1: A c= B and
A2: LMP B in A and
A3: not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty and
A4: proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_below and
A5: (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) ; :: thesis: LMP A = LMP B
set w = ((W-bound A) + (E-bound A)) / 2;
A6: ( (LMP A) `2 = lower_bound (proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) & not proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is empty ) by A3, Lm1, EUCLID:52, RELAT_1:119;
A7: (LMP B) `1 = ((W-bound A) + (E-bound A)) / 2 by A5, EUCLID:52;
A8: for s being Real st 0 < s holds
ex r being Real st
( r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & r < ((LMP B) `2) + s )
proof
let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & r < ((LMP B) `2) + s ) )
assume A9: 0 < s ; :: thesis: ex r being Real st
( r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & r < ((LMP B) `2) + s )
take (LMP B) `2 ; :: thesis: ( (LMP B) `2 in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & (LMP B) `2 < ((LMP B) `2) + s )
LMP B in Vertical_Line (((W-bound A) + (E-bound A)) / 2) by A7, JORDAN6:31;
then ( proj2 . (LMP B) = (LMP B) `2 & LMP B in A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) ) by A2, PSCOMP_1:def 6, XBOOLE_0:def 4;
hence (LMP B) `2 in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) by FUNCT_2:35; :: thesis: (LMP B) `2 < ((LMP B) `2) + s
((LMP B) `2) + 0 < ((LMP B) `2) + s by A9, XREAL_1:6;
hence (LMP B) `2 < ((LMP B) `2) + s ; :: thesis: verum
end;
A10: A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) c= B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) by A1, XBOOLE_1:26;
then A11: proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) c= proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) by RELAT_1:123;
(LMP B) `2 = lower_bound (proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) by A5, EUCLID:52;
then A12: for r being Real st r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) holds
(LMP B) `2 <= r by A4, A5, A11, SEQ_4:def 2;
proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_below by A4, A5, A10, RELAT_1:123, XXREAL_2:44;
then ( (LMP A) `1 = ((W-bound A) + (E-bound A)) / 2 & (LMP A) `2 = (LMP B) `2 ) by A6, A12, A8, EUCLID:52, SEQ_4:def 2;
hence LMP A = LMP B by A7, TOPREAL3:6; :: thesis: verum