let r be Real; :: thesis: for A being Point of RealSpace st r > 0 holds
A in Ball (A,r)
let A be Point of RealSpace; :: thesis: ( r > 0 implies A in Ball (A,r) )
reconsider A9 = A as Real by METRIC_1:def 13;
A1: abs (A9 - A9) = 0 by ABSVALUE:2;
assume r > 0 ; :: thesis: A in Ball (A,r)
then dist (A,A) < r by A1, TOPMETR:11;
hence A in Ball (A,r) by METRIC_1:11; :: thesis: verum