let C be Simple_closed_curve; :: thesis: for n being Nat st 0 < n holds
ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
let n be Nat; :: thesis: ( 0 < n implies ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & UMP (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 ; :: thesis: ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
then UMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(upper_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 Th13;
then A6: (UMP (L~ (Cage (C,n)))) `2 = upper_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 = upper_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:2;
A13: (UMP (L~ (Cage (C,n)))) `1 = ((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2 by EUCLID:52;
take i ; :: thesis: ( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
thus ( 1 <= i & i <= len (Gauge (C,n)) ) by A10, A11; :: thesis: UMP (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 (UMP (L~ (Cage (C,n)))) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 by A13, JORDAN1G:33;
hence UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) by A12, A6, TOPREAL3:6; :: thesis: verum