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) by SUBSET_1:10;
dist (x,e) < r by A1, METRIC_1:12;
hence contradiction by METRIC_1:5; :: thesis: verum