let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being 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 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:43;
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:10;
A4: (Cage (C,n)) /. m = W-min (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def 6;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then consider i, j being 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 9;
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_0:32; :: thesis: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j)
A8: i <= len (Gauge (C,n)) by A5, MATRIX_0:32;

A9: now :: thesis: not i > 1

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:3;
then W-bound (L~ (Cage (C,n))) > ((Gauge (C,n)) * (1,j)) `1 by EUCLID:52;
hence contradiction by A7, A1, JORDAN1A:73; :: thesis: verum

end;

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