theorem Th5: :: JORDAN5D:5

for h being non constant standard special_circular_sequence
for I, i being Nat st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) holds
( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 )