theorem :: GOBOARD7:12
for f being non empty FinSequence of (TOP-REAL 2)
for i, j being Nat st f is special & i <= len (GoB f) & j <= width (GoB f) holds
Int (cell ((GoB f),i,j)) misses L~ f