let C be Simple_closed_curve; for n being Nat st 0 < n holds
ex i being 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 Nat; ( 0 < n implies ex i being 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));
A1:
Cage (C,n) is_sequence_on Gauge (C,n)
by JORDAN9:def 1;
A2:
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;
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:31;
then A3:
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 JORDAN6:61, XBOOLE_1:63;
A4:
Center (Gauge (C,n)) <= len (Gauge (C,n))
by JORDAN1B:13;
assume A5:
0 < n
; ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
then
LMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(lower_bound (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 Th14;
then A6:
(LMP (L~ (Cage (C,n)))) `2 = lower_bound (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 EUCLID:52;
A7:
1 <= len (Gauge (C,n))
by Lm3;
A8:
1 <= Center (Gauge (C,n))
by JORDAN1B:11;
then A9:
[(Center (Gauge (C,n))),(len (Gauge (C,n)))] in Indices (Gauge (C,n))
by A2, A7, A4, MATRIX_0:30;
[(Center (Gauge (C,n))),1] in Indices (Gauge (C,n))
by A2, A7, A8, A4, MATRIX_0:30;
then consider i being Nat such that
A10:
1 <= i
and
A11:
i <= len (Gauge (C,n))
and
A12:
((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `2 = lower_bound (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 A1, A3, A7, A9, JORDAN1F:1;
A13:
(LMP (L~ (Cage (C,n)))) `1 = ((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2
by EUCLID:52;
take
i
; ( 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 A10, A11; LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i)
((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2
by A5, A2, A10, A11, JORDAN1G:35;
then
(LMP (L~ (Cage (C,n)))) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1
by A13, JORDAN1G:33;
hence
LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i)
by A12, A6, TOPREAL3:6; verum