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 (Cage C,n) & W-min C in right_cell (Cage C,n),i )
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 (Cage C,n) & W-min C in right_cell (Cage C,n),i )
consider i being Element of NAT such that
A1: ( 1 <= i & i < len (Cage C,n) ) and
A2: W-min C in right_cell (Cage C,n),i,(Gauge C,n) by Th21;
take i ; :: thesis: ( 1 <= i & i < len (Cage C,n) & W-min C in right_cell (Cage C,n),i )
thus ( 1 <= i & i < len (Cage C,n) ) by A1; :: thesis: W-min C in right_cell (Cage C,n),i
A3: i + 1 <= len (Cage C,n) by A1, NAT_1:13;
Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
then right_cell (Cage C,n),i,(Gauge C,n) c= right_cell (Cage C,n),i by A1, A3, GOBRD13:34;
hence W-min C in right_cell (Cage C,n),i by A2; :: thesis: verum