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 Element of 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 Element of 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 Element of 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 Element of 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:17;
then A3: Int (right_cell f,k,G) c= (right_cell f,k,G) \ (L~ f) by TOPS_1:44, XBOOLE_1:86;
Int (left_cell f,k,G) misses L~ f by A1, A2, JORDAN9:17;
then A4: Int (left_cell f,k,G) c= (left_cell f,k,G) \ (L~ f) by TOPS_1:44, XBOOLE_1:86;
(right_cell f,k,G) \ (L~ f) c= RightComp f by A1, A2, JORDAN9:29;
hence Int (right_cell f,k,G) c= RightComp f by A3, XBOOLE_1:1; :: thesis: Int (left_cell f,k,G) c= LeftComp f
(left_cell f,k,G) \ (L~ f) c= LeftComp f by A1, A2, JORDAN9:29;
hence Int (left_cell f,k,G) c= LeftComp f by A4, XBOOLE_1:1; :: thesis: verum