theorem :: JORDAN21:45

for A, B being Subset of (TOP-REAL 2) st 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) holds
UMP A = UMP B