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 )
assume A1: r1 <= r2 ; :: thesis: Ball |[a,r1]|,r1 c= Ball |[a,r2]|,r2
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 A2: x in Ball |[a,r1]|,r1 ; :: thesis: x in Ball |[a,r2]|,r2
then reconsider x = x as Element of (TOP-REAL 2) ;
( |[a,r1]| - |[a,r2]| = |[(a - a),(r1 - r2)]| & r1 - r2 is Real ) by EUCLID:66, XREAL_0:def 1;
then |.(|[a,r1]| - |[a,r2]|).| = |.(r1 - r2).| by TOPREAL6:31;
then ( |.(|[a,r1]| - |[a,r2]|).| = |.(r2 - r1).| & r2 - r1 >= 0 ) by A1, COMPLEX1:146, XREAL_1:50;
then ( |.(|[a,r1]| - |[a,r2]|).| = r2 - r1 & |.(x - |[a,r1]|).| < r1 ) by A2, ABSVALUE:def 1, TOPREAL9:7;
then ( |.(x - |[a,r1]|).| + |.(|[a,r1]| - |[a,r2]|).| < r1 + (r2 - r1) & |.(x - |[a,r2]|).| <= |.(x - |[a,r1]|).| + |.(|[a,r1]| - |[a,r2]|).| ) by TOPRNS_1:35, XREAL_1:10;
then |.(x - |[a,r2]|).| < r2 by XXREAL_0:2;
hence x in Ball |[a,r2]|,r2 by TOPREAL9:7; :: thesis: verum