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 } & dist u,u = 0 ) by METRIC_1:1, METRIC_1:18;
assume r > 0 ; :: thesis: u in Ball u,r
hence u in Ball u,r by A1; :: thesis: verum