theorem Th11: :: JORDAN5D:11

for h being non constant standard special_circular_sequence
for i being Nat st 1 <= i & i <= len h holds
( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) )