let X be RealUnitarySpace; :: 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) )
A1: dist (x,x) = 0 by BHSP_1:34;
assume r > 0 ; :: thesis: x in Ball (x,r)
hence x in Ball (x,r) by A1, Th41; :: thesis: verum