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