let X be ComplexUnitarySpace; :: thesis: for y, x being Point of X
for r being Real st y in Ball x,r holds
y in cl_Ball x,r
let y, x be Point of X; :: thesis: for r being Real st y in Ball x,r holds
y in cl_Ball x,r
let r be Real; :: thesis: ( y in Ball x,r implies y in cl_Ball x,r )
assume y in Ball x,r ; :: thesis: y in cl_Ball x,r
then ||.(x - y).|| <= r by Th40;
hence y in cl_Ball x,r ; :: thesis: verum