let k be Nat; :: thesis: for G being Go-board
for f, g being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special & L~ g c= L~ f & 1 <= k & k + 1 <= len f holds
for A being Subset of (TOP-REAL 2) st ( A = (right_cell (f,k,G)) \ (L~ g) or A = (left_cell (f,k,G)) \ (L~ g) ) holds
A is connected
let G be Go-board; :: thesis: for f, g being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special & L~ g c= L~ f & 1 <= k & k + 1 <= len f holds
for A being Subset of (TOP-REAL 2) st ( A = (right_cell (f,k,G)) \ (L~ g) or A = (left_cell (f,k,G)) \ (L~ g) ) holds
A is connected
let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & f is special & L~ g c= L~ f & 1 <= k & k + 1 <= len f implies for A being Subset of (TOP-REAL 2) st ( A = (right_cell (f,k,G)) \ (L~ g) or A = (left_cell (f,k,G)) \ (L~ g) ) holds
A is connected )
assume that
A1: f is_sequence_on G and
A2: f is special and
A3: L~ g c= L~ f and
A4: ( 1 <= k & k + 1 <= len f ) ; :: thesis: for A being Subset of (TOP-REAL 2) st ( A = (right_cell (f,k,G)) \ (L~ g) or A = (left_cell (f,k,G)) \ (L~ g) ) holds
A is connected
let A be Subset of (TOP-REAL 2); :: thesis: ( ( A = (right_cell (f,k,G)) \ (L~ g) or A = (left_cell (f,k,G)) \ (L~ g) ) implies A is connected )
assume A5: ( A = (right_cell (f,k,G)) \ (L~ g) or A = (left_cell (f,k,G)) \ (L~ g) ) ; :: thesis: A is connected

per cases ( A = (right_cell (f,k,G)) \ (L~ g) or A = (left_cell (f,k,G)) \ (L~ g) ) by A5;

suppose A6: A = (right_cell (f,k,G)) \ (L~ g) ; :: thesis: A is connected

Int (right_cell (f,k,G)) misses L~ f by A1, A2, A4, Th15;
then Int (right_cell (f,k,G)) misses L~ g by A3, XBOOLE_1:63;
then A7: Int (right_cell (f,k,G)) c= (L~ g) ` by SUBSET_1:23;
A c= right_cell (f,k,G) by A6, XBOOLE_1:36;
then A8: A c= Cl (Int (right_cell (f,k,G))) by A1, A4, Th11;
A9: A = (right_cell (f,k,G)) /\ ((L~ g) `) by A6, SUBSET_1:13;
( Int (right_cell (f,k,G)) is convex & Int (right_cell (f,k,G)) c= right_cell (f,k,G) ) by A1, A4, Th10, TOPS_1:16;
hence A is connected by A9, A7, A8, CONNSP_1:18, XBOOLE_1:19; :: thesis: verum

end;

suppose A10: A = (left_cell (f,k,G)) \ (L~ g) ; :: thesis: A is connected

Int (left_cell (f,k,G)) misses L~ f by A1, A2, A4, Th15;
then Int (left_cell (f,k,G)) misses L~ g by A3, XBOOLE_1:63;
then A11: Int (left_cell (f,k,G)) c= (L~ g) ` by SUBSET_1:23;
A c= left_cell (f,k,G) by A10, XBOOLE_1:36;
then A12: A c= Cl (Int (left_cell (f,k,G))) by A1, A4, Th11;
A13: A = (left_cell (f,k,G)) /\ ((L~ g) `) by A10, SUBSET_1:13;
( Int (left_cell (f,k,G)) is convex & Int (left_cell (f,k,G)) c= left_cell (f,k,G) ) by A1, A4, Th10, TOPS_1:16;
hence A is connected by A13, A11, A12, CONNSP_1:18, XBOOLE_1:19; :: thesis: verum

end;

end;