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