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

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