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
Sphere 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
Sphere x,r c= Ball x,s
let x be Point of (TOP-REAL n); :: thesis: ( r < s implies Sphere x,r c= Ball x,s )
assume r < s ; :: thesis: Sphere x,r c= Ball x,s
then A1: cl_Ball x,r c= Ball x,s by Th21;
Sphere x,r c= cl_Ball x,r by TOPREAL9:17;
hence Sphere x,r c= Ball x,s by A1, XBOOLE_1:1; :: thesis: verum