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