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: ( W-bound C = W-bound (Lower_Arc C) & E-bound C = E-bound (Lower_Arc C) ) by Th28, Th29;
A2: not proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty by Th31;
A3: proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_below by Th13;
Lower_Arc C c= C by JORDAN6:76;
then (Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) c= C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by XBOOLE_1:26;
then A4: inf (proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) >= inf (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by A2, A3, RELAT_1:156, SEQ_4:64;
A5: (LMP (Lower_Arc C)) `2 = inf (proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by A1, EUCLID:56;
A6: (LMP C) `2 = inf (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:56;
S-bound C <= (LMP C) `2 by Th53;
hence S-bound C <= (LMP (Lower_Arc C)) `2 by A4, A5, A6, XXREAL_0:2; :: thesis: verum