theorem Th65: :: JORDAN:65

for n being non zero Element of NAT
for o, p being Point of (TOP-REAL n)
for r being positive Real st p in Ball (o,r) holds
(DiskProj (o,r,p)) | (Sphere (o,r)) = id (Sphere (o,r))