let X be ComplexUnitarySpace; 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; for r being Real holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)
let r be Real; (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)
then A2:
cl_Ball (x,r) c= (Ball (x,r)) \/ (Sphere (x,r))
by SUBSET_1:2;
( 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; verum