theorem Th34: :: JORDAN5D:34

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 <= len (GoB h) holds
p `2 <= ((GoB h) * (I,(width (GoB h)))) `2