let X be RealUnitarySpace; :: 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 BHSP_1:34;

hence x in cl_Ball (x,r) by Th48; :: thesis: verum

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 BHSP_1:34;

hence x in cl_Ball (x,r) by Th48; :: thesis: verum