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