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

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

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

then consider M' being non empty MetrStruct , p' being Element of M' such that
A1: ( M' = M & p' = p ) and
Ball p,r = { q where q is Element of M' : dist p',q < r } by Def15;

now

let x be Element of M'; :: thesis: ( x in Ball p',r implies x in cl_Ball p',r )
assume x in Ball p',r ; :: thesis: x in cl_Ball p',r
then dist p',x <= r by Th12;
then x in { q where q is Element of M' : dist p',q <= r } ;
hence x in cl_Ball p',r by Lm7; :: thesis: verum

end;

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

end;

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

then ( Ball p,r is empty & cl_Ball p,r is empty ) by Def15, Def16;
hence Ball p,r c= cl_Ball p,r ; :: thesis: verum

end;

end;