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 14;
A1: abs (A9 - A9) = 0 by ABSVALUE:7;
assume r > 0 ; :: thesis: A in Ball (A,r)
then dist (A,A) < r by A1, TOPMETR:15;
hence A in Ball (A,r) by METRIC_1:12; :: thesis: verum