let C be Simple_closed_curve; :: thesis: for n being Element of NAT st 0 < n holds
ex i being Element of NAT st
( 1 <= i & i <= len (Gauge C,n) & LMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i )
let n be Element of NAT ; :: thesis: ( 0 < n implies ex i being Element of NAT st
( 1 <= i & i <= len (Gauge C,n) & LMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i ) )
assume A1: 0 < n ; :: thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge C,n) & LMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i )
set f = Cage C,n;
set G = Gauge C,n;
set w = Center (Gauge C,n);
A2: LMP (L~ (Cage C,n)) = |[(((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2),(inf (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))))]| by A1, Th14;
A3: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
A4: LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) meets Upper_Arc (L~ (Cage C,n)) by JORDAN1B:34;
Upper_Arc (L~ (Cage C,n)) c= L~ (Cage C,n) by JORDAN6:76;
then A5: LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) meets L~ (Cage C,n) by A4, XBOOLE_1:63;
A6: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A7: 1 <= len (Gauge C,n) by Lm3;
( 1 <= Center (Gauge C,n) & Center (Gauge C,n) <= len (Gauge C,n) ) by JORDAN1B:12, JORDAN1B:14;
then ( [(Center (Gauge C,n)),1] in Indices (Gauge C,n) & [(Center (Gauge C,n)),(len (Gauge C,n))] in Indices (Gauge C,n) ) by A6, A7, MATRIX_1:37;
then consider i being Element of NAT such that
A8: ( 1 <= i & i <= len (Gauge C,n) ) and
A9: ((Gauge C,n) * (Center (Gauge C,n)),i) `2 = inf (proj2 .: ((LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))) /\ (L~ (Cage C,n)))) by A3, A5, A7, JORDAN1F:1;
take i ; :: thesis: ( 1 <= i & i <= len (Gauge C,n) & LMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i )
thus ( 1 <= i & i <= len (Gauge C,n) ) by A8; :: thesis: LMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i
A10: (LMP (L~ (Cage C,n))) `2 = inf (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))) by A2, EUCLID:56;
A11: (LMP (L~ (Cage C,n))) `1 = ((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2 by EUCLID:56;
((Gauge C,n) * (Center (Gauge C,n)),i) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, A6, A8, JORDAN1G:43;
then (LMP (L~ (Cage C,n))) `1 = ((Gauge C,n) * (Center (Gauge C,n)),i) `1 by A11, JORDAN1G:41;
hence LMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i by A9, A10, TOPREAL3:11; :: thesis: verum