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