theorem Th22: :: JORDAN1A:22

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 <= len G holds
(G * (t,1)) `2 <= S-bound (L~ f)