theorem Th21: :: JORDAN1A:21

for t being Nat
for G being Go-board
for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= width G holds
(G * (1,t)) `1 <= W-bound (L~ f)