let X be RealUnitarySpace; :: thesis: for x being Point of X

for r being Real holds Ball (x,r) c= cl_Ball (x,r)

let x be Point of X; :: thesis: for r being Real holds Ball (x,r) c= cl_Ball (x,r)

let r be Real; :: thesis: Ball (x,r) c= cl_Ball (x,r)

for y being Point of X st y in Ball (x,r) holds

y in cl_Ball (x,r) by Th50;

hence Ball (x,r) c= cl_Ball (x,r) by SUBSET_1:2; :: thesis: verum

for r being Real holds Ball (x,r) c= cl_Ball (x,r)

let x be Point of X; :: thesis: for r being Real holds Ball (x,r) c= cl_Ball (x,r)

let r be Real; :: thesis: Ball (x,r) c= cl_Ball (x,r)

for y being Point of X st y in Ball (x,r) holds

y in cl_Ball (x,r) by Th50;

hence Ball (x,r) c= cl_Ball (x,r) by SUBSET_1:2; :: thesis: verum