let n be Element of NAT ; :: thesis: for r being real number
for x being Point of (TOP-REAL n) holds Sphere (x,r) c= cl_Ball (x,r)
let r be real number ; :: thesis: for x being Point of (TOP-REAL n) holds Sphere (x,r) c= cl_Ball (x,r)
let x be Point of (TOP-REAL n); :: thesis: Sphere (x,r) c= cl_Ball (x,r)
reconsider e = x as Point of (Euclid n) by TOPREAL3:8;
( Sphere (x,r) = Sphere (e,r) & cl_Ball (x,r) = cl_Ball (e,r) ) by Th14, Th15;
hence Sphere (x,r) c= cl_Ball (x,r) by METRIC_1:15; :: thesis: verum