let X be ComplexUnitarySpace; :: 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