theorem :: JORDAN1H:25

for G being Go-board
for f being non constant standard special_circular_sequence st f is_sequence_on G holds
for k being Nat st 1 <= k & k + 1 <= len f holds
( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f )