let X be RealUnitarySpace; :: thesis: for x, z being Point of X

for r being Real holds

( z in Sphere (x,r) iff ||.(x - z).|| = r )

let x, z be Point of X; :: thesis: for r being Real holds

( z in Sphere (x,r) iff ||.(x - z).|| = r )

let r be Real; :: thesis: ( z in Sphere (x,r) iff ||.(x - z).|| = r )

thus ( z in Sphere (x,r) implies ||.(x - z).|| = r ) :: thesis: ( ||.(x - z).|| = r implies z in Sphere (x,r) )

hence z in Sphere (x,r) ; :: thesis: verum

for r being Real holds

( z in Sphere (x,r) iff ||.(x - z).|| = r )

let x, z be Point of X; :: thesis: for r being Real holds

( z in Sphere (x,r) iff ||.(x - z).|| = r )

let r be Real; :: thesis: ( z in Sphere (x,r) iff ||.(x - z).|| = r )

thus ( z in Sphere (x,r) implies ||.(x - z).|| = r ) :: thesis: ( ||.(x - z).|| = r implies z in Sphere (x,r) )

proof

assume
||.(x - z).|| = r
; :: thesis: z in Sphere (x,r)
assume
z in Sphere (x,r)
; :: thesis: ||.(x - z).|| = r

then ex y being Point of X st

( z = y & ||.(x - y).|| = r ) ;

hence ||.(x - z).|| = r ; :: thesis: verum

end;then ex y being Point of X st

( z = y & ||.(x - y).|| = r ) ;

hence ||.(x - z).|| = r ; :: thesis: verum

hence z in Sphere (x,r) ; :: thesis: verum