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