let X be ComplexUnitarySpace; :: thesis: for x being Point of X
for r being Real st r >= 0 holds
x in cl_Ball x,r
let x be Point of X; :: thesis: for r being Real st r >= 0 holds
x in cl_Ball x,r
let r be Real; :: thesis: ( r >= 0 implies x in cl_Ball x,r )
assume r >= 0 ; :: thesis: x in cl_Ball x,r
then dist x,x <= r by CSSPACE:53;
hence x in cl_Ball x,r by Th48; :: thesis: verum