let N be non empty MetrStruct ; :: thesis: for w being Element of N
for r being Real st N is Reflexive & 0 < r holds
w in Ball (w,r)
let w be Element of N; :: thesis: for r being Real st N is Reflexive & 0 < r holds
w in Ball (w,r)
let r be Real; :: thesis: ( N is Reflexive & 0 < r implies w in Ball (w,r) )
assume N is Reflexive ; :: thesis: ( not 0 < r or w in Ball (w,r) )
then A1: dist (w,w) = 0 by METRIC_1:1;
assume 0 < r ; :: thesis: w in Ball (w,r)
hence w in Ball (w,r) by A1, METRIC_1:11; :: thesis: verum