let C be Simple_closed_curve; :: thesis: (UMP (Upper_Arc C)) `2 <= N-bound C
set w = ((E-bound C) + (W-bound C)) / 2;
A1: ( W-bound C = W-bound (Upper_Arc C) & E-bound C = E-bound (Upper_Arc C) ) by Th26, Th27;
A2: not proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty by Th30;
A3: proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above by Th13;
Upper_Arc C c= C by JORDAN6:76;
then (Upper_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: sup (proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) <= sup (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by A2, A3, RELAT_1:156, SEQ_4:65;
A5: (UMP (Upper_Arc C)) `2 = sup (proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by A1, EUCLID:56;
A6: (UMP C) `2 = sup (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:56;
(UMP C) `2 <= N-bound C by Th52;
hence (UMP (Upper_Arc C)) `2 <= N-bound C by A4, A5, A6, XXREAL_0:2; :: thesis: verum