let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for r, s being Real st r + |.(p - q).| <= s holds
Ball (p,r) c= Ball (q,s)
let p, q be Point of (TOP-REAL n); :: thesis: for r, s being Real st r + |.(p - q).| <= s holds
Ball (p,r) c= Ball (q,s)
let r, s be Real; :: thesis: ( r + |.(p - q).| <= s implies Ball (p,r) c= Ball (q,s) )
assume A1: r + |.(p - q).| <= s ; :: thesis: Ball (p,r) c= Ball (q,s)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (p,r) or x in Ball (q,s) )
assume A2: x in Ball (p,r) ; :: thesis: x in Ball (q,s)
then reconsider x = x as Point of (TOP-REAL n) ;
|.(x - p).| + |.(p - q).| < r + |.(p - q).| by A2, TOPREAL9:7, XREAL_1:6;
then A3: |.(x - p).| + |.(p - q).| < s by A1, XXREAL_0:2;
A4: x is Element of REAL n by EUCLID:22;
A5: p is Element of REAL n by EUCLID:22;
q is Element of REAL n by EUCLID:22;
then |.(x - q).| <= |.(x - p).| + |.(p - q).| by A4, A5, EUCLID:19;
then |.(x - q).| < s by A3, XXREAL_0:2;
hence x in Ball (q,s) ; :: thesis: verum