let N be non empty MetrStruct ; :: thesis: for w being Element of N
for r being real number st N is Reflexive & 0 < r holds
w in Ball w,r
let w be Element of N; :: thesis: for r being real number st N is Reflexive & 0 < r holds
w in Ball w,r
let r be real number ; :: 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:12; :: thesis: verum