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 & i <= len (Gauge C,n) & 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, SPRECT_2:45; :: thesis: verum