let A, B be Subset of (TOP-REAL 2); :: thesis: ( A c= B & UMP 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_above & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) implies UMP A = UMP B )
assume that
A1: A c= B and
A2: UMP 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_above and
A5: (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) ; :: thesis: UMP A = UMP B
set w = ((W-bound A) + (E-bound A)) / 2;
A6: ( (UMP A) `2 = upper_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: (UMP 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))) & ((UMP B) `2) - s < r )

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))) & ((UMP B) `2) - s < r ) )
assume A9: 0 < s ; :: thesis: ex r being Real st
( r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & ((UMP B) `2) - s < r )
take (UMP B) `2 ; :: thesis: ( (UMP B) `2 in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & ((UMP B) `2) - s < (UMP B) `2 )
UMP B in Vertical_Line (((W-bound A) + (E-bound A)) / 2) by A7, JORDAN6:31;
then ( proj2 . (UMP B) = (UMP B) `2 & UMP B in A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) ) by A2, PSCOMP_1:def 6, XBOOLE_0:def 4;
hence (UMP B) `2 in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) by FUNCT_2:35; :: thesis: ((UMP B) `2) - s < (UMP B) `2
((UMP B) `2) - s < ((UMP B) `2) - 0 by A9, XREAL_1:15;
hence ((UMP B) `2) - s < (UMP B) `2 ; :: 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;
(UMP B) `2 = upper_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
(UMP B) `2 >= r by A4, A5, A11, SEQ_4:def 1;
proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_above by A4, A5, A10, RELAT_1:123, XXREAL_2:43;
then ( (UMP A) `1 = ((W-bound A) + (E-bound A)) / 2 & (UMP A) `2 = (UMP B) `2 ) by A6, A12, A8, EUCLID:52, SEQ_4:def 1;
hence UMP A = UMP B by A7, TOPREAL3:6; :: thesis: verum