let p be Point of (TOP-REAL 2); :: thesis: for C being compact Subset of (TOP-REAL 2) st p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) holds
(LMP C) `2 <= p `2
let C be compact Subset of (TOP-REAL 2); :: thesis: ( p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) implies (LMP C) `2 <= p `2 )
assume A1: p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) ; :: thesis: (LMP C) `2 <= p `2
p `2 = proj2 . p by PSCOMP_1:def 6;
then A2: p `2 in proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A1, FUNCT_2:35;
( (LMP C) `2 = lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) & not proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_below ) by A1, Lm1, Th13, EUCLID:52, RELAT_1:119;
hence (LMP C) `2 <= p `2 by A2, SEQ_4:def 2; :: thesis: verum