let X be RealUnitarySpace; for x, y being Point of X
for r being Real st y in Sphere (x,r) holds
y in cl_Ball (x,r)
let x, y be Point of X; for r being Real st y in Sphere (x,r) holds
y in cl_Ball (x,r)
let r be Real; ( y in Sphere (x,r) implies y in cl_Ball (x,r) )
assume
y in Sphere (x,r)
; y in cl_Ball (x,r)
then
||.(x - y).|| = r
by Th51;
hence
y in cl_Ball (x,r)
; verum