theorem Th62: :: TOPGEN_5:62

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