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

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

suppose not M is empty ; :: thesis: cl_Ball p,r c= (Sphere p,r) \/ (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 cl_Ball p9,r implies x in (Sphere p9,r) \/ (Ball p9,r) )
assume x in cl_Ball p9,r ; :: thesis: x in (Sphere p9,r) \/ (Ball p9,r)
then A2: dist p9,x <= r by Th13;

now

per cases ( dist p9,x < r or dist p9,x = r ) by A2, XXREAL_0:1;

case dist p9,x < r ; :: thesis: x in Ball p9,r

hence x in Ball p9,r by Th12; :: thesis: verum

end;

case dist p9,x = r ; :: thesis: x in Sphere p9,r

hence x in Sphere p9,r by Th14; :: thesis: verum

end;

end;

end;

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

end;

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

end;

suppose A3: M is empty ; :: thesis: cl_Ball p,r c= (Sphere p,r) \/ (Ball p,r)

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

end;

end;