theorem Th12: :: JORDAN5D:12

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