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

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