let C be Simple_closed_curve; :: thesis: for n being Element of NAT st 0 < n holds
LMP (L~ (Cage C,n)) = LMP (Lower_Arc (L~ (Cage C,n)))
let n be Element of NAT ; :: thesis: ( 0 < n implies LMP (L~ (Cage C,n)) = LMP (Lower_Arc (L~ (Cage C,n))) )
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: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 (Lower_Arc (L~ (Cage C,n))) by JORDAN21:29;
A4: W-bound (L~ (Cage C,n)) = W-bound (Lower_Arc (L~ (Cage C,n))) by JORDAN21:28;
assume A5: 0 < n ; :: thesis: LMP (L~ (Cage C,n)) = LMP (Lower_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: 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: contradiction
consider j being Element of 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, 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);
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:69;
LMP (L~ (Cage C,n)) in L~ (Cage C,n) by JORDAN21:44;
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 set 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:12;
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:59;
then A22: ((Gauge C,n) * (Center (Gauge C,n)),j) `1 = ((E-bound C) + (W-bound C)) / 2 by A5, A13, A14, A20, JORDAN1A:57;
then LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,n) * (Center (Gauge C,n)),j) is vertical by A21, SPPOL_1:37;
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:42;
A26: Center (Gauge C,n) <= len (Gauge C,n) by JORDAN1B:14;
1 <= Center (Gauge C,1) by JORDAN1B:12;
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:64;
((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:24;
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:10;
(LMP (L~ (Cage C,n))) `2 <= (LMP (Lower_Arc (L~ (Cage C,n)))) `2 by A1, A2, A4, A3, A24, JORDAN21:13, JORDAN21:57;
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:11; :: thesis: verum

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:31, JORDAN21:59; :: thesis: verum