let n be Element of NAT ; :: thesis: for a, b being Element of (TOP-REAL n)
for r1, r2 being real positive number 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 real positive number st |.(a - b).| <= r1 - r2 holds
Ball b,r2 c= Ball a,r1
let r1, r2 be real positive number ; :: 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:28;
let x be set ; :: 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:10;
|.(x - a).| <= |.(x - b).| + |.(b - a).| by TOPRNS_1:35;
then |.(x - a).| < r2 + (r1 - r2) by A3, XXREAL_0:2;
hence x in Ball a,r1 by TOPREAL9:7; :: thesis: verum