let k be Nat; 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; 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); ( 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 )
; 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); ( ( 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) )
; 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)
;
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;
verum end; suppose A10:
A = (left_cell (f,k,G)) \ (L~ g)
;
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;
verum end;