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