let k be Element of 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 & f is special & L~ g c= L~ f ) and
A2: 1 <= k and
A3: 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 A4: ( 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 A4;

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

then A6: A = (right_cell f,k,G) /\ ((L~ g) ` ) by SUBSET_1:32;
A7: A c= right_cell f,k,G by A5, XBOOLE_1:36;
A8: Int (right_cell f,k,G) is connected by A1, A2, A3, Th12;
Int (right_cell f,k,G) misses L~ f by A1, A2, A3, Th17;
then Int (right_cell f,k,G) misses L~ g by A1, XBOOLE_1:63;
then A9: Int (right_cell f,k,G) c= (L~ g) ` by SUBSET_1:43;
A10: Int (right_cell f,k,G) c= right_cell f,k,G by TOPS_1:44;
A c= Cl (Int (right_cell f,k,G)) by A1, A2, A3, A7, Th13;
hence A is connected by A6, A8, A9, A10, CONNSP_1:19, XBOOLE_1:19; :: thesis: verum

end;

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

then A12: A = (left_cell f,k,G) /\ ((L~ g) ` ) by SUBSET_1:32;
A13: A c= left_cell f,k,G by A11, XBOOLE_1:36;
A14: Int (left_cell f,k,G) is connected by A1, A2, A3, Th12;
Int (left_cell f,k,G) misses L~ f by A1, A2, A3, Th17;
then Int (left_cell f,k,G) misses L~ g by A1, XBOOLE_1:63;
then A15: Int (left_cell f,k,G) c= (L~ g) ` by SUBSET_1:43;
A16: Int (left_cell f,k,G) c= left_cell f,k,G by TOPS_1:44;
A c= Cl (Int (left_cell f,k,G)) by A1, A2, A3, A13, Th13;
hence A is connected by A12, A14, A15, A16, CONNSP_1:19, XBOOLE_1:19; :: thesis: verum

end;

end;