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