let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being 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 Nat st
( 1 <= i & i < len (Cage (C,n)) & W-min 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 Nat such that
A2: 1 <= i and
A3: i < len (Cage (C,n)) and
A4: W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th17;
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 A2, A3; :: thesis: W-min 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:33;
hence W-min C in right_cell ((Cage (C,n)),i) by A4; :: thesis: verum