let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2)
for i, j being Element of NAT st f is_sequence_on G & f is special & i <= len G & j <= width G holds
(cell G,i,j) \ (L~ f) is connected
let f be FinSequence of (TOP-REAL 2); :: thesis: for i, j being Element of NAT st f is_sequence_on G & f is special & i <= len G & j <= width G holds
(cell G,i,j) \ (L~ f) is connected
let i, j be Element of NAT ; :: thesis: ( f is_sequence_on G & f is special & i <= len G & j <= width G implies (cell G,i,j) \ (L~ f) is connected )
assume that
A1: ( f is_sequence_on G & f is special ) and
A2: ( i <= len G & j <= width G ) ; :: thesis: (cell G,i,j) \ (L~ f) is connected
A3: (cell G,i,j) \ (L~ f) = (cell G,i,j) /\ ((L~ f) ` ) by SUBSET_1:32;
A4: (cell G,i,j) \ (L~ f) c= cell G,i,j by XBOOLE_1:36;
Int (cell G,i,j) misses L~ f by A1, A2, JORDAN9:16;
then A5: Int (cell G,i,j) c= (L~ f) ` by SUBSET_1:43;
Int (cell G,i,j) c= cell G,i,j by TOPS_1:44;
then A6: Int (cell G,i,j) c= (cell G,i,j) \ (L~ f) by A3, A5, XBOOLE_1:19;
(cell G,i,j) \ (L~ f) c= Cl (Int (cell G,i,j)) by A2, A4, GOBRD11:35;
hence (cell G,i,j) \ (L~ f) is connected by A2, A6, CONNSP_1:19, GOBOARD9:21; :: thesis: verum