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:76, 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, Th31;
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:156, SEQ_4:64;
( W-bound C = W-bound (Lower_Arc C) & E-bound C = E-bound (Lower_Arc C) ) by Th28, Th29;
then A3: (LMP (Lower_Arc C)) `2 = lower_bound (proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:56;
( (LMP C) `2 = lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) & S-bound C <= (LMP C) `2 ) by Th53, EUCLID:56;
hence S-bound C <= (LMP (Lower_Arc C)) `2 by A2, A3, XXREAL_0:2; :: thesis: verum