let r, s be real number ; :: thesis: 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 ; :: thesis: 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); :: thesis: ( r < s implies cl_Ball x,r c= Ball x,s )
assume A1: r < s ; :: thesis: cl_Ball x,r c= Ball x,s
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in cl_Ball x,r or a in Ball x,s )
assume A2: a in cl_Ball x,r ; :: thesis: 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; :: thesis: verum