let G be Go-board; :: thesis: 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 )
let f be non constant standard special_circular_sequence; :: thesis: ( f is_sequence_on G implies 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 ) )
assume A1: f is_sequence_on G ; :: thesis: 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 )
let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies ( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f ) )
assume A2: ( 1 <= k & k + 1 <= len f ) ; :: thesis: ( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f )
Int (right_cell (f,k,G)) misses L~ f by A1, A2, JORDAN9:15;
then A3: Int (right_cell (f,k,G)) c= (right_cell (f,k,G)) \ (L~ f) by TOPS_1:16, XBOOLE_1:86;
Int (left_cell (f,k,G)) misses L~ f by A1, A2, JORDAN9:15;
then A4: Int (left_cell (f,k,G)) c= (left_cell (f,k,G)) \ (L~ f) by TOPS_1:16, XBOOLE_1:86;
(right_cell (f,k,G)) \ (L~ f) c= RightComp f by A1, A2, JORDAN9:27;
hence Int (right_cell (f,k,G)) c= RightComp f by A3; :: thesis: Int (left_cell (f,k,G)) c= LeftComp f
(left_cell (f,k,G)) \ (L~ f) c= LeftComp f by A1, A2, JORDAN9:27;
hence Int (left_cell (f,k,G)) c= LeftComp f by A4; :: thesis: verum