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 :: thesis: for y being Point of X st y in cl_Ball (x,r) holds
y in (Ball (x,r)) \/ (Sphere (x,r))
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 :: thesis: ( ( ||.(x - y).|| < r & y in Ball (x,r) ) or ( ||.(x - y).|| = r & y in Sphere (x,r) ) )
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: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; :: thesis: verum