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 ;

A1: |.(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

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 ;

A1: |.(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