let C be Simple_closed_curve; :: thesis: for n being Element of NAT st 0 < n holds
UMP (L~ (Cage C,n)) = UMP (Upper_Arc (L~ (Cage C,n)))
let n be Element of NAT ; :: thesis: ( 0 < n implies UMP (L~ (Cage C,n)) = UMP (Upper_Arc (L~ (Cage C,n))) )
set f = Cage C,n;
set w = ((E-bound C) + (W-bound C)) / 2;
A1: Upper_Arc (L~ (Cage C,n)) c= L~ (Cage C,n) by JORDAN6:76;
A2: (W-bound C) + (E-bound C) = (W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n))) by JORDAN1G:41;
A3: E-bound (L~ (Cage C,n)) = E-bound (Upper_Arc (L~ (Cage C,n))) by JORDAN21:27;
A4: W-bound (L~ (Cage C,n)) = W-bound (Upper_Arc (L~ (Cage C,n))) by JORDAN21:26;
assume A5: 0 < n ; :: thesis: UMP (L~ (Cage C,n)) = UMP (Upper_Arc (L~ (Cage C,n)))
then A6: 0 + 1 <= n by NAT_1:13;
then A7: (n -' 1) + 1 = n by XREAL_1:237;

A8: now

A9: Center (Gauge C,1) <= len (Gauge C,1) by JORDAN1B:14;
A10: Center (Gauge C,n) <= len (Gauge C,n) by JORDAN1B:14;
A11: (Upper_Arc (L~ (Cage C,n))) \/ (Lower_Arc (L~ (Cage C,n))) = L~ (Cage C,n) by JORDAN6:def 9;
assume A12: not UMP (L~ (Cage C,n)) in Upper_Arc (L~ (Cage C,n)) ; :: thesis: contradiction
UMP (L~ (Cage C,n)) in L~ (Cage C,n) by JORDAN21:43;
then A13: UMP (L~ (Cage C,n)) in Lower_Arc (L~ (Cage C,n)) by A12, A11, XBOOLE_0:def 3;
A14: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A15: 1 <= Center (Gauge C,n) by JORDAN1B:12;
consider j being Element of NAT such that
A16: 1 <= j and
A17: j <= len (Gauge C,n) and
A18: UMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),j by A5, Th21;
set a = (Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1));
set b = (Gauge C,n) * (Center (Gauge C,n)),j;
set L = LSeg ((Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1))),((Gauge C,n) * (Center (Gauge C,n)),j);
len (Gauge C,1) = width (Gauge C,1) by JORDAN8:def 1;
then LSeg ((Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1))),((Gauge C,n) * (Center (Gauge C,n)),j) meets Upper_Arc (L~ (Cage C,n)) by A7, A13, A16, A17, A18, A14, JORDAN19:5;
then consider x being set such that
A19: x in LSeg ((Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1))),((Gauge C,n) * (Center (Gauge C,n)),j) and
A20: x in Upper_Arc (L~ (Cage C,n)) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A19;
A21: (Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1)) in LSeg ((Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1))),((Gauge C,n) * (Center (Gauge C,n)),j) by RLTOPSP1:69;
A22: 1 <= len (Gauge C,1) by Lm3;
then A23: ((Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1))) `1 = ((E-bound C) + (W-bound C)) / 2 by JORDAN1A:59;
then A24: ((Gauge C,n) * (Center (Gauge C,n)),j) `1 = ((E-bound C) + (W-bound C)) / 2 by A5, A16, A17, A22, JORDAN1A:57;
then LSeg ((Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1))),((Gauge C,n) * (Center (Gauge C,n)),j) is vertical by A23, SPPOL_1:37;
then A25: x `1 = ((E-bound C) + (W-bound C)) / 2 by A19, A23, A21, SPPOL_1:def 3;
then x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ;
then A26: x in (Upper_Arc (L~ (Cage C,n))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A20, XBOOLE_0:def 4;
then A27: (UMP (Upper_Arc (L~ (Cage C,n)))) `2 >= x `2 by A2, A4, A3, JORDAN21:41;
1 <= Center (Gauge C,1) by JORDAN1B:12;
then A28: ((Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1))) `2 >= ((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) `2 by A6, A15, A10, A9, JORDAN1A:61;
len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then ((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) `2 >= ((Gauge C,n) * (Center (Gauge C,n)),j) `2 by A16, A17, A15, A10, SPRECT_3:24;
then ((Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1))) `2 >= ((Gauge C,n) * (Center (Gauge C,n)),j) `2 by A28, XXREAL_0:2;
then A29: x `2 >= ((Gauge C,n) * (Center (Gauge C,n)),j) `2 by A19, TOPREAL1:10;
(UMP (L~ (Cage C,n))) `2 >= (UMP (Upper_Arc (L~ (Cage C,n)))) `2 by A1, A2, A4, A3, A26, JORDAN21:13, JORDAN21:56;
then ((Gauge C,n) * (Center (Gauge C,n)),j) `2 >= x `2 by A18, A27, XXREAL_0:2;
then ((Gauge C,n) * (Center (Gauge C,n)),j) `2 = x `2 by A29, XXREAL_0:1;
hence contradiction by A12, A18, A20, A24, A25, TOPREAL3:11; :: thesis: verum

end;

proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above by A2, JORDAN21:13;
hence UMP (L~ (Cage C,n)) = UMP (Upper_Arc (L~ (Cage C,n))) by A1, A2, A4, A3, A8, JORDAN21:30, JORDAN21:58; :: thesis: verum