theorem Th15: :: TOPREAL9:17

for n being Nat
for r being Real
for x being Point of (TOP-REAL n) holds Sphere (x,r) c= cl_Ball (x,r)