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;
assume A1: 0 < n ; :: thesis: UMP (L~ (Cage C,n)) = UMP (Upper_Arc (L~ (Cage C,n)))
then A2: 0 + 1 <= n by NAT_1:13;
then A3: (n -' 1) + 1 = n by XREAL_1:237;
A4: Upper_Arc (L~ (Cage C,n)) c= L~ (Cage C,n) by JORDAN6:76;
A5: (W-bound C) + (E-bound C) = (W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n))) by JORDAN1G:41;
then A6: proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above by JORDAN21:13;
A7: ( W-bound (L~ (Cage C,n)) = W-bound (Upper_Arc (L~ (Cage C,n))) & E-bound (L~ (Cage C,n)) = E-bound (Upper_Arc (L~ (Cage C,n))) ) by JORDAN21:26, JORDAN21:27;
then A8: not (Upper_Arc (L~ (Cage C,n))) /\ (Vertical_Line (((W-bound (Upper_Arc (L~ (Cage C,n)))) + (E-bound (Upper_Arc (L~ (Cage C,n))))) / 2)) is empty by JORDAN21:30;

now

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

end;

hence UMP (L~ (Cage C,n)) = UMP (Upper_Arc (L~ (Cage C,n))) by A4, A5, A6, A7, A8, JORDAN21:58; :: thesis: verum