let r be Real; :: thesis:
let M be MetrStruct ; :: thesis:
let p be Element of M; :: thesis:
( Sphere (p,r) c= cl_Ball (p,r) & Ball (p,r) c= cl_Ball (p,r) ) by Th14, Th15;
hence (Sphere (p,r)) \/ (Ball (p,r)) c= cl_Ball (p,r) by XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis:

per cases ;

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

now :: thesis:

let x be Element of M; :: thesis:
assume x in cl_Ball (p,r) ; :: thesis:
then A2: dist (p,x) <= r by Th12;

now :: thesis:

per cases by A2, XXREAL_0:1;

case dist (p,x) < r ; :: thesis:

hence x in Ball (p,r) by A1, Th11; :: thesis:

end;

case dist (p,x) = r ; :: thesis:

hence x in Sphere (p,r) by A1, Th13; :: thesis:

end;

end;

end;

hence x in (Sphere (p,r)) \/ (Ball (p,r)) by XBOOLE_0:def 3; :: thesis:

end;

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

end;

suppose A3: M is empty ; :: thesis:

then ( Ball (p,r) is empty & cl_Ball (p,r) is empty ) ;
hence cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r)) by A3, Def16; :: thesis:

end;

end;