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