let M be non empty Reflexive MetrStruct ; :: thesis: for u being Point of M
for r being real number st r > 0 holds
u in Ball u,r
let u be Point of M; :: thesis: for r being real number st r > 0 holds
u in Ball u,r
let r be real number ; :: thesis: ( r > 0 implies u in Ball u,r )
A1: Ball u,r = { q where q is Point of M : dist u,q < r } by METRIC_1:18;
assume A2: r > 0 ; :: thesis: u in Ball u,r
dist u,u = 0 by METRIC_1:1;
hence u in Ball u,r by A1, A2; :: thesis: verum