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
( (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 Element of 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 Element of 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 Element of 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, Th11;
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:44, XBOOLE_1:7;
then A4: Int (right_cell f,k,G) c= ((right_cell f,k,G) \ (L~ f)) \/ (L~ f) by XBOOLE_1:1;
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:32;
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:34, XBOOLE_1:36;
then (right_cell f,k,G) \ (L~ f) c= right_cell f,k by XBOOLE_1:1;
then A6: Int ((right_cell f,k,G) \ (L~ f)) c= Int (right_cell f,k) by TOPS_1:48;
Int (right_cell f,k) c= RightComp f by A2, GOBOARD9:28;
then A7: Int ((right_cell f,k,G) \ (L~ f)) c= RightComp f by A6, XBOOLE_1:1;
Int (right_cell f,k,G) misses L~ f by A1, A2, Th17;
then A8: Int (Int (right_cell f,k,G)) c= Int ((right_cell f,k,G) \ (L~ f)) by A4, TOPS_1:48, XBOOLE_1:73;
Int (right_cell f,k,G) c= (right_cell f,k,G) \ (L~ f) by A1, A2, A4, Th17, 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, Th28;
hence (right_cell f,k,G) \ (L~ f) c= RightComp f by A7, A9, A5, GOBOARD9:6; :: 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:32;
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:44, XBOOLE_1:7;
then A11: Int (left_cell f,k,G) c= ((left_cell f,k,G) \ (L~ f)) \/ (L~ f) by XBOOLE_1:1;
( (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:34, XBOOLE_1:36;
then (left_cell f,k,G) \ (L~ f) c= left_cell f,k by XBOOLE_1:1;
then A12: Int ((left_cell f,k,G) \ (L~ f)) c= Int (left_cell f,k) by TOPS_1:48;
Int (left_cell f,k) c= LeftComp f by A2, GOBOARD9:24;
then A13: Int ((left_cell f,k,G) \ (L~ f)) c= LeftComp f by A12, XBOOLE_1:1;
A14: Int (left_cell f,k,G) <> {} by A1, A2, Th11;
Int (left_cell f,k,G) misses L~ f by A1, A2, Th17;
then A15: Int (Int (left_cell f,k,G)) c= Int ((left_cell f,k,G) \ (L~ f)) by A11, TOPS_1:48, XBOOLE_1:73;
Int (left_cell f,k,G) c= (left_cell f,k,G) \ (L~ f) by A1, A2, A11, Th17, 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, Th28;
hence (left_cell f,k,G) \ (L~ f) c= LeftComp f by A13, A16, A10, GOBOARD9:6; :: thesis: verum