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:7; :: thesis: verum