let X be RealUnitarySpace; :: thesis: for x being Point of X
for r being Real holds (Ball x,r) \/ (Sphere x,r) = cl_Ball x,r
let x be Point of X; :: thesis: for r being Real holds (Ball x,r) \/ (Sphere x,r) = cl_Ball x,r
let r be Real; :: thesis: (Ball x,r) \/ (Sphere x,r) = cl_Ball x,r
A1: (Ball x,r) \/ (Sphere x,r) c= cl_Ball x,r

proof

( Ball x,r c= cl_Ball x,r & Sphere x,r c= cl_Ball x,r ) by Th54, Th55;
hence (Ball x,r) \/ (Sphere x,r) c= cl_Ball x,r by XBOOLE_1:8; :: thesis: verum

end;

now

let y be Point of X; :: thesis: ( y in cl_Ball x,r implies y in (Ball x,r) \/ (Sphere x,r) )
assume y in cl_Ball x,r ; :: thesis: y in (Ball x,r) \/ (Sphere x,r)
then A2: ||.(x - y).|| <= r by Th47;

now

per cases ( ||.(x - y).|| < r or ||.(x - y).|| = r ) by A2, XXREAL_0:1;

case ||.(x - y).|| < r ; :: thesis: y in Ball x,r

hence y in Ball x,r ; :: thesis: verum

end;

case ||.(x - y).|| = r ; :: thesis: y in Sphere x,r

hence y in Sphere x,r ; :: thesis: verum

end;

end;

end;

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

end;

then cl_Ball x,r c= (Ball x,r) \/ (Sphere x,r) by SUBSET_1:7;
hence (Ball x,r) \/ (Sphere x,r) = cl_Ball x,r by A1, XBOOLE_0:def 10; :: thesis: verum