let n be Element of NAT ; :: thesis: for r being real number
for y, x being Point of (TOP-REAL n) holds
( y in Sphere (x,r) iff |.(y - x).| = r )
let r be real number ; :: thesis: for y, x being Point of (TOP-REAL n) holds
( y in Sphere (x,r) iff |.(y - x).| = r )
let y, x be Point of (TOP-REAL n); :: thesis: ( y in Sphere (x,r) iff |.(y - x).| = r )

hereby :: thesis: ( |.(y - x).| = r implies y in Sphere (x,r) )

assume y in Sphere (x,r) ; :: thesis: |.(y - x).| = r
then ex p being Point of (TOP-REAL n) st
( y = p & |.(p - x).| = r ) ;
hence |.(y - x).| = r ; :: thesis: verum

end;

thus ( |.(y - x).| = r implies y in Sphere (x,r) ) ; :: thesis: verum