let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2)
for i, j being 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 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 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 and
A2: f is special and
A3: i <= len G and
A4: j <= width G ; :: thesis: (cell (G,i,j)) \ (L~ f) is connected
Int (cell (G,i,j)) misses L~ f by A1, A2, A3, A4, JORDAN9:14;
then A5: Int (cell (G,i,j)) c= (L~ f) ` by SUBSET_1:23;
(cell (G,i,j)) \ (L~ f) c= cell (G,i,j) by XBOOLE_1:36;
then A6: (cell (G,i,j)) \ (L~ f) c= Cl (Int (cell (G,i,j))) by A3, A4, GOBRD11:35;
A7: Int (cell (G,i,j)) c= cell (G,i,j) by TOPS_1:16;
A8: Int (cell (G,i,j)) is convex by A3, A4, GOBOARD9:17;
(cell (G,i,j)) \ (L~ f) = (cell (G,i,j)) /\ ((L~ f) `) by SUBSET_1:13;
then Int (cell (G,i,j)) c= (cell (G,i,j)) \ (L~ f) by A5, A7, XBOOLE_1:19;
hence (cell (G,i,j)) \ (L~ f) is connected by A6, A8, CONNSP_1:18; :: thesis: verum