let r, s be Real; :: 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; :: thesis: verum