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

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