theorem Th32: :: JORDAN5D:32

for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence
for I being Nat st p in L~ h & 1 <= I & I <= width (GoB h) holds
p `1 <= ((GoB h) * ((len (GoB h)),I)) `1