assume not cl_Ball (p,r) is empty ; :: thesis: contradiction
then consider x being object such that
A1: x in cl_Ball (p,r) ;
reconsider x = x as Element of (EMINFTY n) by A1;
dist (x,p) <= r by A1, METRIC_1:12;
hence contradiction by METRIC_1:5; :: thesis: verum