let a be real number ; :: thesis: for r1, r2 being real positive number st r1 <= r2 holds
Ball (|[a,r1]|,r1) c= Ball (|[a,r2]|,r2)
let r1, r2 be real positive number ; :: thesis: ( r1 <= r2 implies Ball (|[a,r1]|,r1) c= Ball (|[a,r2]|,r2) )
A1: r1 - r2 is Real by XREAL_0:def 1;
assume r1 <= r2 ; :: thesis: Ball (|[a,r1]|,r1) c= Ball (|[a,r2]|,r2)
then A2: r2 - r1 >= 0 by XREAL_1:48;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (|[a,r1]|,r1) or x in Ball (|[a,r2]|,r2) )
assume A3: x in Ball (|[a,r1]|,r1) ; :: thesis: x in Ball (|[a,r2]|,r2)
then reconsider x = x as Element of (TOP-REAL 2) ;
A4: |.(x - |[a,r1]|).| < r1 by A3, TOPREAL9:7;
|[a,r1]| - |[a,r2]| = |[(a - a),(r1 - r2)]| by EUCLID:62;
then |.(|[a,r1]| - |[a,r2]|).| = |.(r1 - r2).| by A1, TOPREAL6:23;
then |.(|[a,r1]| - |[a,r2]|).| = |.(r2 - r1).| by COMPLEX1:60;
then |.(|[a,r1]| - |[a,r2]|).| = r2 - r1 by A2, ABSVALUE:def 1;
then A5: |.(x - |[a,r1]|).| + |.(|[a,r1]| - |[a,r2]|).| < r1 + (r2 - r1) by A4, XREAL_1:8;
|.(x - |[a,r2]|).| <= |.(x - |[a,r1]|).| + |.(|[a,r1]| - |[a,r2]|).| by TOPRNS_1:34;
then |.(x - |[a,r2]|).| < r2 by A5, XXREAL_0:2;
hence x in Ball (|[a,r2]|,r2) by TOPREAL9:7; :: thesis: verum