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

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:2; :: thesis: verum