theorem Th31: :: JORDAN5D:31

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
((GoB h) * (1,I)) `1 <= p `1