let X be RealUnitarySpace; :: thesis: for x, z being Point of X
for r being Real holds
( z in Sphere (x,r) iff dist (x,z) = r )
let x, z be Point of X; :: thesis: for r being Real holds
( z in Sphere (x,r) iff dist (x,z) = r )
let r be Real; :: thesis: ( z in Sphere (x,r) iff dist (x,z) = r )
thus ( z in Sphere (x,r) implies dist (x,z) = r ) :: thesis: ( dist (x,z) = r implies z in Sphere (x,r) )

proof

assume z in Sphere (x,r) ; :: thesis: dist (x,z) = r
then ||.(x - z).|| = r by Th51;
hence dist (x,z) = r by BHSP_1:def 5; :: thesis: verum

end;

assume dist (x,z) = r ; :: thesis: z in Sphere (x,r)
then ||.(x - z).|| = r by BHSP_1:def 5;
hence z in Sphere (x,r) ; :: thesis: verum