assume
not Ball (e,r) is empty
; :: thesis: contradiction

then consider x being Point of (Euclid n) such that

A1: x in Ball (e,r) ;

dist (x,e) < r by A1, METRIC_1:11;

hence contradiction by METRIC_1:5; :: thesis: verum

then consider x being Point of (Euclid n) such that

A1: x in Ball (e,r) ;

dist (x,e) < r by A1, METRIC_1:11;

hence contradiction by METRIC_1:5; :: thesis: verum