theorem :: GOBRD13:30

for k being Nat
for f being FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
right_cell (f,k,G) is closed