let C be Simple_closed_curve; :: thesis:
let n be Element of NAT ; :: thesis:
set f = Cage C,n;
set w = ((E-bound C) + (W-bound C)) / 2;
assume A1: 0 < n ; :: thesis:
then A2: 0 + 1 <= n by NAT_1:13;
then A3: (n -' 1) + 1 = n by XREAL_1:237;
A4: Lower_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_below by JORDAN21:13;
A7: ( W-bound (L~ (Cage C,n)) = W-bound (Lower_Arc (L~ (Cage C,n))) & E-bound (L~ (Cage C,n)) = E-bound (Lower_Arc (L~ (Cage C,n))) ) by JORDAN21:28, JORDAN21:29;
then A8: not (Lower_Arc (L~ (Cage C,n))) /\ (Vertical_Line (((W-bound (Lower_Arc (L~ (Cage C,n)))) + (E-bound (Lower_Arc (L~ (Cage C,n))))) / 2)) is empty by JORDAN21:31;

now

assume A9: not LMP (L~ (Cage C,n)) in Lower_Arc (L~ (Cage C,n)) ; :: thesis:
A10: LMP (L~ (Cage C,n)) in L~ (Cage C,n) by JORDAN21:44;
(Upper_Arc (L~ (Cage C,n))) \/ (Lower_Arc (L~ (Cage C,n))) = L~ (Cage C,n) by JORDAN6:def 9;
then A11: LMP (L~ (Cage C,n)) in Upper_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: LMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),j by A1, Th22;
set a = (Gauge C,1) * (Center (Gauge C,1)),1;
set b = (Gauge C,n) * (Center (Gauge C,n)),j;
set L = LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,n) * (Center (Gauge C,n)),j);
A14: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,n) * (Center (Gauge C,n)),j) meets Lower_Arc (L~ (Cage C,n)) by A3, A11, A12, A13, JORDAN1J:62;
then consider x being set such that
A15: x in LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,n) * (Center (Gauge C,n)),j) and
A16: x in Lower_Arc (L~ (Cage C,n)) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A15;
A17: 1 <= len (Gauge C,1) by Lm3;
then A18: ((Gauge C,1) * (Center (Gauge C,1)),1) `1 = ((E-bound C) + (W-bound C)) / 2 by JORDAN1A:59;
then A19: ((Gauge C,n) * (Center (Gauge C,n)),j) `1 = ((E-bound C) + (W-bound C)) / 2 by A1, A12, A17, JORDAN1A:57;
then A20: LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,n) * (Center (Gauge C,n)),j) is vertical by A18, SPPOL_1:37;
A21: ( 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 A22: ((Gauge C,1) * (Center (Gauge C,1)),1) `2 <= ((Gauge C,n) * (Center (Gauge C,n)),1) `2 by A2, A21, JORDAN1A:64;
((Gauge C,n) * (Center (Gauge C,n)),1) `2 <= ((Gauge C,n) * (Center (Gauge C,n)),j) `2 by A12, A14, A21, SPRECT_3:24;
then ((Gauge C,1) * (Center (Gauge C,1)),1) `2 <= ((Gauge C,n) * (Center (Gauge C,n)),j) `2 by A22, XXREAL_0:2;
then A23: x `2 <= ((Gauge C,n) * (Center (Gauge C,n)),j) `2 by A15, TOPREAL1:10;
(Gauge C,1) * (Center (Gauge C,1)),1 in LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,n) * (Center (Gauge C,n)),j) by RLTOPSP1:69;
then A24: x `1 = ((E-bound C) + (W-bound C)) / 2 by A15, A18, A20, SPPOL_1:def 3;
then x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ;
then A25: x in (Lower_Arc (L~ (Cage C,n))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A16, XBOOLE_0:def 4;
then A26: (LMP (Lower_Arc (L~ (Cage C,n)))) `2 <= x `2 by A5, A7, JORDAN21:42;
(LMP (L~ (Cage C,n))) `2 <= (LMP (Lower_Arc (L~ (Cage C,n)))) `2 by A4, A5, A6, A7, A25, JORDAN21:57;
then ((Gauge C,n) * (Center (Gauge C,n)),j) `2 <= x `2 by A13, A26, XXREAL_0:2;
then ((Gauge C,n) * (Center (Gauge C,n)),j) `2 = x `2 by A23, XXREAL_0:1;
hence contradiction by A9, A13, A16, A19, A24, TOPREAL3:11; :: thesis:

end;

hence LMP (L~ (Cage C,n)) = LMP (Lower_Arc (L~ (Cage C,n))) by A4, A5, A6, A7, A8, JORDAN21:59; :: thesis: