let C be Simple_closed_curve; :: thesis: for n being Nat st 0 < n holds
UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n))))
let n be 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:61;
A2: (W-bound C) + (E-bound C) = (W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n)))) by JORDAN1G:33;
A3: E-bound (L~ (Cage (C,n))) = E-bound (Upper_Arc (L~ (Cage (C,n)))) by JORDAN21:18;
A4: W-bound (L~ (Cage (C,n))) = W-bound (Upper_Arc (L~ (Cage (C,n)))) by JORDAN21:17;
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:235;

A8: now :: thesis: UMP (L~ (Cage (C,n))) in Upper_Arc (L~ (Cage (C,n)))

A9: Center (Gauge (C,1)) <= len (Gauge (C,1)) by JORDAN1B:13;
A10: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13;
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:30;
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:11;
consider j being 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, Th19;
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 object 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:68;
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:38;
then A24: ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `1 = ((E-bound C) + (W-bound C)) / 2 by A5, A16, A17, A22, JORDAN1A:36;
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:16;
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:28;
1 <= Center (Gauge (C,1)) by JORDAN1B:11;
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:40;
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:12;
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:4;
(UMP (L~ (Cage (C,n)))) `2 >= (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 by A1, A2, A4, A3, A26, JORDAN21:13, JORDAN21:43;
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:6; :: 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:21, JORDAN21:45; :: thesis: verum