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 M' being non empty MetrStruct , p' being Element of M' such that
A1: ( M' = M & p' = p ) and
Sphere p,r = { q where q is Element of M' : dist p',q = r } by Def17;

now

let x be Element of M'; :: thesis: ( x in cl_Ball p',r implies x in (Sphere p',r) \/ (Ball p',r) )
assume x in cl_Ball p',r ; :: thesis: x in (Sphere p',r) \/ (Ball p',r)
then A2: dist p',x <= r by Th13;

now

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

case dist p',x < r ; :: thesis: x in Ball p',r

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

end;

case dist p',x = r ; :: thesis: x in Sphere p',r

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

end;

end;

end;

hence x in (Sphere p',r) \/ (Ball p',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 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 & Sphere p,r is empty ) by Def15, Def16, Def17;
hence cl_Ball p,r c= (Sphere p,r) \/ (Ball p,r) ; :: thesis: verum

end;

end;