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:53;

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:28; :: 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:28
.= 0 ;
:: thesis: verum