theorem Th55: :: TOPREALC:55

for n, m being Nat
for r being Real
for p being Point of (TOP-REAL m) st n in dom p holds
(PROJ (m,n)) .: (Ball (p,r)) = ].((p /. n) - r),((p /. n) + r).[