for p being Point of (TOP-REAL 2) st p `2 >= 0 holds
for x being Real
for y being non negative Real
for r being positive Real holds
( (+ (x,y,r)) . p = 0 iff p = |[x,y]| )