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