let X be RealUnitarySpace; :: thesis: 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; :: thesis: for r being Real st y in Sphere (x,r) holds

y in cl_Ball (x,r)

let r be Real; :: thesis: ( y in Sphere (x,r) implies y in cl_Ball (x,r) )

assume y in Sphere (x,r) ; :: thesis: y in cl_Ball (x,r)

then ||.(x - y).|| = r by Th51;

hence y in cl_Ball (x,r) ; :: thesis: verum

for r being Real st y in Sphere (x,r) holds

y in cl_Ball (x,r)

let x, y be Point of X; :: thesis: for r being Real st y in Sphere (x,r) holds

y in cl_Ball (x,r)

let r be Real; :: thesis: ( y in Sphere (x,r) implies y in cl_Ball (x,r) )

assume y in Sphere (x,r) ; :: thesis: y in cl_Ball (x,r)

then ||.(x - y).|| = r by Th51;

hence y in cl_Ball (x,r) ; :: thesis: verum