let X be ComplexUnitarySpace; :: 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

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 A1: ||.(x - y).|| <= r by Th47;

now

per cases ( ||.(x - y).|| < r or ||.(x - y).|| = r ) by A1, 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 A2: cl_Ball x,r c= (Ball x,r) \/ (Sphere x,r) by SUBSET_1:7;
( Ball x,r c= cl_Ball x,r & Sphere x,r c= cl_Ball x,r ) by Th54, Th55;
then (Ball x,r) \/ (Sphere x,r) c= cl_Ball x,r by XBOOLE_1:8;
hence (Ball x,r) \/ (Sphere x,r) = cl_Ball x,r by A2, XBOOLE_0:def 10; :: thesis: verum