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
p `2 <= (UMP C) `2
let C be compact Subset of (TOP-REAL 2); :: thesis: ( p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) implies p `2 <= (UMP C) `2 )
assume A1: p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) ; :: thesis: p `2 <= (UMP C) `2
A2: (UMP C) `2 = sup (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:56;
A3: ( 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_above ) by A1, Lm1, Th13, RELAT_1:152;
p `2 = proj2 . p by PSCOMP_1:def 29;
then p `2 in proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A1, FUNCT_2:43;
hence p `2 <= (UMP C) `2 by A2, A3, SEQ_4:def 4; :: thesis: verum