let k be Element of NAT ; :: thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & 1 <= k & k + 1 <= len f holds
( f /. k in left_cell f,k,G & f /. k in right_cell f,k,G )
let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & 1 <= k & k + 1 <= len f holds
( f /. k in left_cell f,k,G & f /. k in right_cell f,k,G )
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f implies ( f /. k in left_cell f,k,G & f /. k in right_cell f,k,G ) )
assume that
A1: f is_sequence_on G and
A2: ( 1 <= k & k + 1 <= len f ) ; :: thesis: ( f /. k in left_cell f,k,G & f /. k in right_cell f,k,G )
set p = f /. k;
LSeg f,k = LSeg (f /. k),(f /. (k + 1)) by A2, TOPREAL1:def 5;
then f /. k in LSeg f,k by RLTOPSP1:69;
then f /. k in (left_cell f,k,G) /\ (right_cell f,k,G) by A1, A2, GOBRD13:30;
hence ( f /. k in left_cell f,k,G & f /. k in right_cell f,k,G ) by XBOOLE_0:def 4; :: thesis: verum