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