theorem Th22: :: GOBOARD8:22

for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `1 > ((GoB f) * ((len (GoB f)),1)) `1 ) holds
P misses L~ f