let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,n) & W-min (L~ (Cage C,n)) = (Gauge C,n) * 1,j )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,n) & W-min (L~ (Cage C,n)) = (Gauge C,n) * 1,j )
A1: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
then consider m being Nat such that
A2: m in dom (Cage C,n) and
A3: (Cage C,n) . m = W-min (L~ (Cage C,n)) by FINSEQ_2:11;
A4: (Cage C,n) /. m = W-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 j ; :: thesis: ( 1 <= j & j <= width (Gauge C,n) & W-min (L~ (Cage C,n)) = (Gauge C,n) * 1,j )
thus A7: ( 1 <= j & j <= width (Gauge C,n) ) by A5, MATRIX_1:39; :: thesis: W-min (L~ (Cage C,n)) = (Gauge C,n) * 1,j
A8: i <= len (Gauge C,n) by A5, MATRIX_1:39;

A9: now

assume i > 1 ; :: thesis: contradiction
then (W-min (L~ (Cage C,n))) `1 > ((Gauge C,n) * 1,j) `1 by A4, A6, A7, A8, GOBOARD5:4;
then W-bound (L~ (Cage C,n)) > ((Gauge C,n) * 1,j) `1 by EUCLID:56;
hence contradiction by A7, A1, JORDAN1A:94; :: thesis: verum

end;

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