let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge C,n) & N-min (L~ (Cage C,n)) = (Gauge C,n) * i,(width (Gauge C,n)) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge C,n) & N-min (L~ (Cage C,n)) = (Gauge C,n) * i,(width (Gauge C,n)) )
A1: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
N-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:43;
then consider m being Nat such that
A2: m in dom (Cage C,n) and
A3: (Cage C,n) . m = N-min (L~ (Cage C,n)) by FINSEQ_2:11;
A4: (Cage C,n) /. m = N-min (L~ (Cage C,n)) by A2, A3, PARTFUN1:def 8;
Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
then consider i, j being Element of NAT such that
A5: [i,j] in Indices (Gauge C,n) and
A6: (Cage C,n) /. m = (Gauge C,n) * i,j by A2, GOBOARD1:def 11;
take i ; :: thesis: ( 1 <= i & i <= len (Gauge C,n) & N-min (L~ (Cage C,n)) = (Gauge C,n) * i,(width (Gauge C,n)) )
thus A7: ( 1 <= i & i <= len (Gauge C,n) ) by A5, MATRIX_1:39; :: thesis: N-min (L~ (Cage C,n)) = (Gauge C,n) * i,(width (Gauge C,n))
A8: 1 <= j by A5, MATRIX_1:39;

A9: now

assume j < width (Gauge C,n) ; :: thesis: contradiction
then (N-min (L~ (Cage C,n))) `2 < ((Gauge C,n) * i,(width (Gauge C,n))) `2 by A4, A6, A7, A8, GOBOARD5:5;
then N-bound (L~ (Cage C,n)) < ((Gauge C,n) * i,(width (Gauge C,n))) `2 by EUCLID:56;
hence contradiction by A7, A1, JORDAN1A:91; :: thesis: verum

end;

j <= width (Gauge C,n) by A5, MATRIX_1:39;
hence N-min (L~ (Cage C,n)) = (Gauge C,n) * i,(width (Gauge C,n)) by A4, A6, A9, XXREAL_0:1; :: thesis: verum