let M be non empty Reflexive MetrStruct ; :: thesis: for u being Point of M
for r being Real st r > 0 holds
u in Ball (u,r)
let u be Point of M; :: thesis: for r being Real st r > 0 holds
u in Ball (u,r)
let r be Real; :: 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:17;
assume r > 0 ; :: thesis: u in Ball (u,r)
hence u in Ball (u,r) by A1; :: thesis: verum