let X be RealUnitarySpace; :: thesis: for z, x being Point of X
for r being Real holds
( z in Sphere x,r iff dist x,z = r )
let z, x 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