let C be Simple_closed_curve; :: thesis: S-bound C <= (LMP (Lower_Arc C)) `2
set w = ((E-bound C) + (W-bound C)) / 2;
A1: (Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) c= C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by JORDAN6:61, XBOOLE_1:26;
( not proj2 .: ((Lower_Arc 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 Th13, Th22;
then A2: lower_bound (proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) >= lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by A1, RELAT_1:123, SEQ_4:47;
( W-bound C = W-bound (Lower_Arc C) & E-bound C = E-bound (Lower_Arc C) ) by Th19, Th20;
then A3: (LMP (Lower_Arc C)) `2 = lower_bound (proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52;
( (LMP C) `2 = lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) & S-bound C <= (LMP C) `2 ) by Th40, EUCLID:52;
hence S-bound C <= (LMP (Lower_Arc C)) `2 by A2, A3, XXREAL_0:2; :: thesis: verum