let n be Nat; :: thesis: for r being Real
for x being Point of (TOP-REAL n) holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)
let r be Real; :: thesis: for x being Point of (TOP-REAL n) holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)
let x be Point of (TOP-REAL n); :: thesis: (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)
reconsider e = x as Point of (Euclid n) by TOPREAL3:8;
A1: cl_Ball (x,r) = cl_Ball (e,r) by Th12;
( Sphere (x,r) = Sphere (e,r) & Ball (x,r) = Ball (e,r) ) by Th11, Th13;
hence (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r) by A1, METRIC_1:16; :: thesis: verum