theorem Th64: :: TOPGEN_5:64

for p being Point of (TOP-REAL 2) st p `2 >= 0 holds
for x, a being Real
for r being positive Real st 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a holds
(+ (x,r)) . p > a