let C be Simple_closed_curve; :: thesis:
let n be Nat; :: thesis:
set f = Cage (C,n);
set w = ((E-bound C) + (W-bound C)) / 2;
A1: Lower_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 (Lower_Arc (L~ (Cage (C,n)))) by JORDAN21:20;
A4: W-bound (L~ (Cage (C,n))) = W-bound (Lower_Arc (L~ (Cage (C,n)))) by JORDAN21:19;
assume A5: 0 < n ; :: thesis:
then A6: 0 + 1 <= n by NAT_1:13;
then A7: (n -' 1) + 1 = n by XREAL_1:235;

A8: now :: thesis:

A9: Center (Gauge (C,1)) <= len (Gauge (C,1)) by JORDAN1B:13;
A10: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A11: (Upper_Arc (L~ (Cage (C,n)))) \/ (Lower_Arc (L~ (Cage (C,n)))) = L~ (Cage (C,n)) by JORDAN6:def 9;
assume A12: not LMP (L~ (Cage (C,n))) in Lower_Arc (L~ (Cage (C,n))) ; :: thesis:
consider j being Nat such that
A13: 1 <= j and
A14: j <= len (Gauge (C,n)) and
A15: LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),j) by A5, Th20;
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)));
A16: (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:68;
LMP (L~ (Cage (C,n))) in L~ (Cage (C,n)) by JORDAN21:31;
then LMP (L~ (Cage (C,n))) in Upper_Arc (L~ (Cage (C,n))) by A12, A11, XBOOLE_0:def 3;
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 A7, A13, A14, A15, A10, JORDAN1J:62;
then consider x being object such that
A17: x in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) and
A18: x in Lower_Arc (L~ (Cage (C,n))) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A17;
A19: 1 <= Center (Gauge (C,n)) by JORDAN1B:11;
A20: 1 <= len (Gauge (C,1)) by Lm3;
then A21: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((E-bound C) + (W-bound C)) / 2 by JORDAN1A:38;
then A22: ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `1 = ((E-bound C) + (W-bound C)) / 2 by A5, A13, A14, A20, JORDAN1A:36;
then LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) is vertical by A21, SPPOL_1:16;
then A23: x `1 = ((E-bound C) + (W-bound C)) / 2 by A17, A21, A16, SPPOL_1:def 3;
then x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ;
then A24: x in (Lower_Arc (L~ (Cage (C,n)))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A18, XBOOLE_0:def 4;
then A25: (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 <= x `2 by A2, A4, A3, JORDAN21:29;
A26: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13;
1 <= Center (Gauge (C,1)) by JORDAN1B:11;
then A27: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `2 by A6, A19, A26, A9, JORDAN1A:43;
((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A13, A14, A10, A19, A26, SPRECT_3:12;
then ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A27, XXREAL_0:2;
then A28: x `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A17, TOPREAL1:4;
(LMP (L~ (Cage (C,n)))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 by A1, A2, A4, A3, A24, JORDAN21:13, JORDAN21:44;
then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 <= x `2 by A15, A25, XXREAL_0:2;
then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 = x `2 by A28, XXREAL_0:1;
hence contradiction by A12, A15, A18, A22, A23, TOPREAL3:6; :: thesis:

end;

proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_below by A2, JORDAN21:13;
hence LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n)))) by A1, A2, A4, A3, A8, JORDAN21:22, JORDAN21:46; :: thesis: