let n be Element of NAT ; :: thesis: for a, b being Element of (TOP-REAL n)
for r1, r2 being positive Real st |.(a - b).| <= r1 - r2 holds
Ball (b,r2) c= Ball (a,r1)
let a, b be Element of (TOP-REAL n); :: thesis: for r1, r2 being positive Real st |.(a - b).| <= r1 - r2 holds
Ball (b,r2) c= Ball (a,r1)
let r1, r2 be positive Real; :: thesis: ( |.(a - b).| <= r1 - r2 implies Ball (b,r2) c= Ball (a,r1) )
assume |.(a - b).| <= r1 - r2 ; :: thesis: Ball (b,r2) c= Ball (a,r1)
then A1: |.(b - a).| <= r1 - r2 by TOPRNS_1:27;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (b,r2) or x in Ball (a,r1) )
assume A2: x in Ball (b,r2) ; :: thesis: x in Ball (a,r1)
then reconsider x = x as Element of (TOP-REAL n) ;
|.(x - b).| < r2 by A2, TOPREAL9:7;
then A3: |.(x - b).| + |.(b - a).| < r2 + (r1 - r2) by A1, XREAL_1:8;
|.(x - a).| <= |.(x - b).| + |.(b - a).| by TOPRNS_1:34;
then |.(x - a).| < r2 + (r1 - r2) by A3, XXREAL_0:2;
hence x in Ball (a,r1) by TOPREAL9:7; :: thesis: verum