let r be Real; :: thesis:
let M be MetrStruct ; :: thesis:
let p be Element of M; :: thesis:

per cases ;

suppose A1: not M is empty ; :: thesis:

now :: thesis:

let x be Element of M; :: thesis:
assume x in Sphere (p,r) ; :: thesis:
then dist (p,x) = r by Th13;
then x in { q where q is Element of M : dist (p,q) <= r } ;
hence x in cl_Ball (p,r) by Def15, A1; :: thesis:

end;

hence Sphere (p,r) c= cl_Ball (p,r) by SUBSET_1:2; :: thesis:

end;

suppose A2: M is empty ; :: thesis:

then Sphere (p,r) is empty ;
hence Sphere (p,r) c= cl_Ball (p,r) by A2, Def15; :: thesis:

end;

end;