theorem :: JORDAN21:46

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