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)

( 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

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))

then A2:
cl_Ball (x,r) c= (Ball (x,r)) \/ (Sphere (x,r))
by SUBSET_1:2;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;

end;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) ) )

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

( 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