theorem Th17: :: JORDAN:17
for n being Element of NAT
for r being non negative Real
for p being Point of (TOP-REAL n) holds p is Point of (Tdisk (p,r))