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 )
set rc = (right_cell f,k,G) \ (L~ f);
A3: (right_cell f,k,G) \ (L~ f) = (right_cell f,k,G) /\ ((L~ f) ` ) by SUBSET_1:32;
A4: (right_cell f,k,G) \ (L~ f) c= right_cell f,k,G by XBOOLE_1:36;
right_cell f,k,G c= right_cell f,k by A1, A2, GOBRD13:34;
then (right_cell f,k,G) \ (L~ f) c= right_cell f,k by A4, XBOOLE_1:1;
then A5: 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 A6: Int ((right_cell f,k,G) \ (L~ f)) c= RightComp f by A5, XBOOLE_1:1;
A7: Int (right_cell f,k,G) <> {} by A1, A2, Th11;
A8: Int (right_cell f,k,G) misses L~ f by A1, A2, Th17;
A9: Int (right_cell f,k,G) c= right_cell f,k,G by TOPS_1:44;
((right_cell f,k,G) \ (L~ f)) \/ (L~ f) = (right_cell f,k,G) \/ (L~ f) by XBOOLE_1:39;
then right_cell f,k,G c= ((right_cell f,k,G) \ (L~ f)) \/ (L~ f) by XBOOLE_1:7;
then A10: Int (right_cell f,k,G) c= ((right_cell f,k,G) \ (L~ f)) \/ (L~ f) by A9, XBOOLE_1:1;
then A11: Int (right_cell f,k,G) c= (right_cell f,k,G) \ (L~ f) by A8, XBOOLE_1:73;
Int (Int (right_cell f,k,G)) c= Int ((right_cell f,k,G) \ (L~ f)) by A8, A10, TOPS_1:48, XBOOLE_1:73;
then A12: (right_cell f,k,G) \ (L~ f) meets Int ((right_cell f,k,G) \ (L~ f)) by A7, A11, XBOOLE_1:68;
A13: (right_cell f,k,G) \ (L~ f) is connected by A1, A2, Th28;
A14: RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
(right_cell f,k,G) \ (L~ f) c= (L~ f) ` by A3, XBOOLE_1:17;
hence (right_cell f,k,G) \ (L~ f) c= RightComp f by A6, A12, A13, A14, GOBOARD9:6; :: thesis: (left_cell f,k,G) \ (L~ f) c= LeftComp f
set lc = (left_cell f,k,G) \ (L~ f);
A15: (left_cell f,k,G) \ (L~ f) = (left_cell f,k,G) /\ ((L~ f) ` ) by SUBSET_1:32;
A16: (left_cell f,k,G) \ (L~ f) c= left_cell f,k,G by XBOOLE_1:36;
left_cell f,k,G c= left_cell f,k by A1, A2, GOBRD13:34;
then (left_cell f,k,G) \ (L~ f) c= left_cell f,k by A16, XBOOLE_1:1;
then A17: 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 A18: Int ((left_cell f,k,G) \ (L~ f)) c= LeftComp f by A17, XBOOLE_1:1;
A19: Int (left_cell f,k,G) <> {} by A1, A2, Th11;
A20: Int (left_cell f,k,G) misses L~ f by A1, A2, Th17;
A21: Int (left_cell f,k,G) c= left_cell f,k,G by TOPS_1:44;
((left_cell f,k,G) \ (L~ f)) \/ (L~ f) = (left_cell f,k,G) \/ (L~ f) by XBOOLE_1:39;
then left_cell f,k,G c= ((left_cell f,k,G) \ (L~ f)) \/ (L~ f) by XBOOLE_1:7;
then A22: Int (left_cell f,k,G) c= ((left_cell f,k,G) \ (L~ f)) \/ (L~ f) by A21, XBOOLE_1:1;
then A23: Int (left_cell f,k,G) c= (left_cell f,k,G) \ (L~ f) by A20, XBOOLE_1:73;
Int (Int (left_cell f,k,G)) c= Int ((left_cell f,k,G) \ (L~ f)) by A20, A22, TOPS_1:48, XBOOLE_1:73;
then A24: (left_cell f,k,G) \ (L~ f) meets Int ((left_cell f,k,G) \ (L~ f)) by A19, A23, XBOOLE_1:68;
A25: (left_cell f,k,G) \ (L~ f) is connected by A1, A2, Th28;
A26: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
(left_cell f,k,G) \ (L~ f) c= (L~ f) ` by A15, XBOOLE_1:17;
hence (left_cell f,k,G) \ (L~ f) c= LeftComp f by A18, A24, A25, A26, GOBOARD9:6; :: thesis: verum