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