theorem Th22: :: JORDAN9:22

for k being Nat
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st 2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k + 1 <= len f holds
ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )