let X be RealUnitarySpace; :: thesis: for x being Point of X
for r being Real holds Sphere x,r c= cl_Ball x,r
let x be Point of X; :: thesis: for r being Real holds Sphere x,r c= cl_Ball x,r
let r be Real; :: thesis: Sphere x,r c= cl_Ball x,r

now

let y be Point of X; :: 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

end;

hence Sphere x,r c= cl_Ball x,r by SUBSET_1:7; :: thesis: verum