let X be ComplexUnitarySpace; for x, w being Point of X
for r being Real holds
( w in Sphere (x,r) iff dist (x,w) = r )
let x, w be Point of X; for r being Real holds
( w in Sphere (x,r) iff dist (x,w) = r )
let r be Real; ( w in Sphere (x,r) iff dist (x,w) = r )
thus
( w in Sphere (x,r) implies dist (x,w) = r )
( dist (x,w) = r implies w in Sphere (x,r) )
assume
dist (x,w) = r
; w in Sphere (x,r)
then
||.(x - w).|| = r
by CSSPACE:def 16;
hence
w in Sphere (x,r)
; verum