let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for k being Nat st 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 implies for k being Nat st 1 <= k & k + 1 <= len f holds
( f /. k in left_cell (f,k,G) & f /. k in right_cell (f,k,G) ) )
assume A1: f is_sequence_on G ; :: thesis: for k being Nat st 1 <= k & k + 1 <= len f holds
( f /. k in left_cell (f,k,G) & f /. k in right_cell (f,k,G) )
let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies ( f /. k in left_cell (f,k,G) & f /. k in right_cell (f,k,G) ) )
assume 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 3;
then f /. k in LSeg (f,k) by RLTOPSP1:68;
then f /. k in (left_cell (f,k,G)) /\ (right_cell (f,k,G)) by A1, A2, GOBRD13:29;
hence ( f /. k in left_cell (f,k,G) & f /. k in right_cell (f,k,G) ) by XBOOLE_0:def 4; :: thesis: verum