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) & (Gauge C,n) * i,(width (Gauge C,n)) in rng (Cage 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) & (Gauge C,n) * i,(width (Gauge C,n)) in rng (Cage C,n) )
consider i being Element of NAT such that
A1: ( 1 <= i & i <= len (Gauge C,n) & N-min (L~ (Cage C,n)) = (Gauge C,n) * i,(width (Gauge C,n)) ) by Th25;
take i ; :: thesis: ( 1 <= i & i <= len (Gauge C,n) & (Gauge C,n) * i,(width (Gauge C,n)) in rng (Cage C,n) )
thus ( 1 <= i & i <= len (Gauge C,n) & (Gauge C,n) * i,(width (Gauge C,n)) in rng (Cage C,n) ) by A1, SPRECT_2:43; :: thesis: verum