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) & (Gauge C,n) * (len (Gauge C,n)),j in rng (Cage C,n) )
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) & (Gauge C,n) * (len (Gauge C,n)),j in rng (Cage C,n) )
consider j being Element of NAT such that
A1: 1 <= j and
A2: j <= width (Gauge C,n) and
A3: E-min (L~ (Cage C,n)) = (Gauge C,n) * (len (Gauge C,n)),j by Th28;
take j ; :: thesis: ( 1 <= j & j <= width (Gauge C,n) & (Gauge C,n) * (len (Gauge C,n)),j in rng (Cage C,n) )
thus ( 1 <= j & j <= width (Gauge C,n) & (Gauge C,n) * (len (Gauge C,n)),j in rng (Cage C,n) ) by A1, A2, A3, SPRECT_2:49; :: thesis: verum