let n be Element of NAT ; :: thesis: for r being real number
for x being Point of (TOP-REAL n) holds (Ball x,r) \/ (Sphere x,r) = cl_Ball x,r
let r be real number ; :: 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:13;
A1: cl_Ball x,r = cl_Ball e,r by Th14;
( Sphere x,r = Sphere e,r & Ball x,r = Ball e,r ) by Th13, Th15;
hence (Ball x,r) \/ (Sphere x,r) = cl_Ball x,r by A1, METRIC_1:17; :: thesis: verum