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: (Upper_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 .: ((Upper_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_above ) by Th13, Th21;
then A2: upper_bound (proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) <= upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by A1, RELAT_1:123, SEQ_4:48;
( W-bound C = W-bound (Upper_Arc C) & E-bound C = E-bound (Upper_Arc C) ) by Th17, Th18;
then A3: (UMP (Upper_Arc C)) `2 = upper_bound (proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52;
( (UMP C) `2 = upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) & (UMP C) `2 <= N-bound C ) by Th39, EUCLID:52;
hence (UMP (Upper_Arc C)) `2 <= N-bound C by A2, A3, XXREAL_0:2; :: thesis: verum