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
( (right_cell (f,k,G)) \ (L~ f) c= RightComp f & (left_cell (f,k,G)) \ (L~ f) 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
( (right_cell (f,k,G)) \ (L~ f) c= RightComp f & (left_cell (f,k,G)) \ (L~ f) c= LeftComp f ) )
assume A1: f is_sequence_on G ; :: thesis: for k being Nat st 1 <= k & k + 1 <= len f holds
( (right_cell (f,k,G)) \ (L~ f) c= RightComp f & (left_cell (f,k,G)) \ (L~ f) c= LeftComp f )
let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies ( (right_cell (f,k,G)) \ (L~ f) c= RightComp f & (left_cell (f,k,G)) \ (L~ f) c= LeftComp f ) )
assume A2: ( 1 <= k & k + 1 <= len f ) ; :: thesis: ( (right_cell (f,k,G)) \ (L~ f) c= RightComp f & (left_cell (f,k,G)) \ (L~ f) c= LeftComp f )
A3: Int (right_cell (f,k,G)) <> {} by A1, A2, Th9;
set rc = (right_cell (f,k,G)) \ (L~ f);
((right_cell (f,k,G)) \ (L~ f)) \/ (L~ f) = (right_cell (f,k,G)) \/ (L~ f) by XBOOLE_1:39;
then ( Int (right_cell (f,k,G)) c= right_cell (f,k,G) & right_cell (f,k,G) c= ((right_cell (f,k,G)) \ (L~ f)) \/ (L~ f) ) by TOPS_1:16, XBOOLE_1:7;
then A4: Int (right_cell (f,k,G)) c= ((right_cell (f,k,G)) \ (L~ f)) \/ (L~ f) ;
set lc = (left_cell (f,k,G)) \ (L~ f);
(right_cell (f,k,G)) \ (L~ f) = (right_cell (f,k,G)) /\ ((L~ f) `) by SUBSET_1:13;
then A5: ( RightComp f is_a_component_of (L~ f) ` & (right_cell (f,k,G)) \ (L~ f) c= (L~ f) ` ) by GOBOARD9:def 2, XBOOLE_1:17;
( (right_cell (f,k,G)) \ (L~ f) c= right_cell (f,k,G) & right_cell (f,k,G) c= right_cell (f,k) ) by A1, A2, GOBRD13:33, XBOOLE_1:36;
then (right_cell (f,k,G)) \ (L~ f) c= right_cell (f,k) ;
then A6: Int ((right_cell (f,k,G)) \ (L~ f)) c= Int (right_cell (f,k)) by TOPS_1:19;
Int (right_cell (f,k)) c= RightComp f by A2, GOBOARD9:25;
then A7: Int ((right_cell (f,k,G)) \ (L~ f)) c= RightComp f by A6;
Int (right_cell (f,k,G)) misses L~ f by A1, A2, Th15;
then A8: Int (Int (right_cell (f,k,G))) c= Int ((right_cell (f,k,G)) \ (L~ f)) by A4, TOPS_1:19, XBOOLE_1:73;
Int (right_cell (f,k,G)) c= (right_cell (f,k,G)) \ (L~ f) by A1, A2, A4, Th15, XBOOLE_1:73;
then A9: (right_cell (f,k,G)) \ (L~ f) meets Int ((right_cell (f,k,G)) \ (L~ f)) by A3, A8, XBOOLE_1:68;
(right_cell (f,k,G)) \ (L~ f) is connected by A1, A2, Th26;
hence (right_cell (f,k,G)) \ (L~ f) c= RightComp f by A7, A9, A5, GOBOARD9:4; :: thesis: (left_cell (f,k,G)) \ (L~ f) c= LeftComp f
(left_cell (f,k,G)) \ (L~ f) = (left_cell (f,k,G)) /\ ((L~ f) `) by SUBSET_1:13;
then A10: ( LeftComp f is_a_component_of (L~ f) ` & (left_cell (f,k,G)) \ (L~ f) c= (L~ f) ` ) by GOBOARD9:def 1, XBOOLE_1:17;
((left_cell (f,k,G)) \ (L~ f)) \/ (L~ f) = (left_cell (f,k,G)) \/ (L~ f) by XBOOLE_1:39;
then ( Int (left_cell (f,k,G)) c= left_cell (f,k,G) & left_cell (f,k,G) c= ((left_cell (f,k,G)) \ (L~ f)) \/ (L~ f) ) by TOPS_1:16, XBOOLE_1:7;
then A11: Int (left_cell (f,k,G)) c= ((left_cell (f,k,G)) \ (L~ f)) \/ (L~ f) ;
( (left_cell (f,k,G)) \ (L~ f) c= left_cell (f,k,G) & left_cell (f,k,G) c= left_cell (f,k) ) by A1, A2, GOBRD13:33, XBOOLE_1:36;
then (left_cell (f,k,G)) \ (L~ f) c= left_cell (f,k) ;
then A12: Int ((left_cell (f,k,G)) \ (L~ f)) c= Int (left_cell (f,k)) by TOPS_1:19;
Int (left_cell (f,k)) c= LeftComp f by A2, GOBOARD9:21;
then A13: Int ((left_cell (f,k,G)) \ (L~ f)) c= LeftComp f by A12;
A14: Int (left_cell (f,k,G)) <> {} by A1, A2, Th9;
Int (left_cell (f,k,G)) misses L~ f by A1, A2, Th15;
then A15: Int (Int (left_cell (f,k,G))) c= Int ((left_cell (f,k,G)) \ (L~ f)) by A11, TOPS_1:19, XBOOLE_1:73;
Int (left_cell (f,k,G)) c= (left_cell (f,k,G)) \ (L~ f) by A1, A2, A11, Th15, XBOOLE_1:73;
then A16: (left_cell (f,k,G)) \ (L~ f) meets Int ((left_cell (f,k,G)) \ (L~ f)) by A14, A15, XBOOLE_1:68;
(left_cell (f,k,G)) \ (L~ f) is connected by A1, A2, Th26;
hence (left_cell (f,k,G)) \ (L~ f) c= LeftComp f by A13, A16, A10, GOBOARD9:4; :: thesis: verum