let r, s be Real; for n being Element of NAT
for x being Point of (TOP-REAL n) st r < s holds
cl_Ball (x,r) c= Ball (x,s)
let n be Element of NAT ; for x being Point of (TOP-REAL n) st r < s holds
cl_Ball (x,r) c= Ball (x,s)
let x be Point of (TOP-REAL n); ( r < s implies cl_Ball (x,r) c= Ball (x,s) )
assume A1:
r < s
; cl_Ball (x,r) c= Ball (x,s)
let a be object ; TARSKI:def 3 ( not a in cl_Ball (x,r) or a in Ball (x,s) )
assume A2:
a in cl_Ball (x,r)
; a in Ball (x,s)
then reconsider a = a as Point of (TOP-REAL n) ;
|.(a - x).| <= r
by A2, TOPREAL9:8;
then
|.(a - x).| < s
by A1, XXREAL_0:2;
hence
a in Ball (x,s)
by TOPREAL9:7; verum