let r be real number ; :: thesis: for M being MetrStruct
for p being Element of M holds Sphere p,r c= cl_Ball p,r
let M be MetrStruct ; :: thesis: for p being Element of M holds Sphere p,r c= cl_Ball p,r
let p be Element of M; :: thesis: Sphere p,r c= cl_Ball p,r

per cases ( not M is empty or M is empty ) ;

suppose not M is empty ; :: thesis: Sphere p,r c= cl_Ball p,r

then consider M9 being non empty MetrStruct , p9 being Element of M9 such that
A1: ( M9 = M & p9 = p ) and
Sphere p,r = { q where q is Element of M9 : dist p9,q = r } by Def17;

now

let x be Element of M9; :: thesis: ( x in Sphere p9,r implies x in cl_Ball p9,r )
assume x in Sphere p9,r ; :: thesis: x in cl_Ball p9,r
then dist p9,x = r by Th14;
then x in { q where q is Element of M9 : dist p9,q <= r } ;
hence x in cl_Ball p9,r by Lm6; :: thesis: verum

end;

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

end;

suppose A2: M is empty ; :: thesis: Sphere p,r c= cl_Ball p,r

then Sphere p,r is empty by Def17;
hence Sphere p,r c= cl_Ball p,r by A2, Def16; :: thesis: verum

end;

end;