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