let p be Point of (TOP-REAL 2); :: thesis: ( p `2 >= 0 implies for x being real number
for y being real non negative number
for r being real positive number holds
( (+ x,y,r) . p = 0 iff p = |[x,y]| ) )
assume A1: p `2 >= 0 ; :: thesis: for x being real number
for y being real non negative number
for r being real positive number holds
( (+ x,y,r) . p = 0 iff p = |[x,y]| )
let x be real number ; :: thesis: for y being real non negative number
for r being real positive number holds
( (+ x,y,r) . p = 0 iff p = |[x,y]| )
let y be real non negative number ; :: thesis: for r being real positive number holds
( (+ x,y,r) . p = 0 iff p = |[x,y]| )
let r be real positive number ; :: thesis: ( (+ x,y,r) . p = 0 iff p = |[x,y]| )
A2: p = |[(p `1 ),(p `2 )]| by EUCLID:57;

hereby :: thesis: ( p = |[x,y]| implies (+ x,y,r) . p = 0 )

assume A3: (+ x,y,r) . p = 0 ; :: thesis: p = |[x,y]|
then p in Ball |[x,y]|,r by A1, A2, Def6;
then 0 = |.(|[x,y]| - p).| / r by A1, A2, A3, Def6;
then 0 * r = |.(|[x,y]| - p).| ;
hence p = |[x,y]| by TOPRNS_1:29; :: thesis: verum

end;

assume A4: p = |[x,y]| ; :: thesis: (+ x,y,r) . p = 0
then p in Ball |[x,y]|,r by Th17;
hence (+ x,y,r) . p = |.(|[x,y]| - p).| / r by A4, Def6
.= 0 / r by A4, TOPRNS_1:29
.= 0 ;
:: thesis: verum