theorem :: MFOLD_0:2

for n being Nat
for p being Point of (TOP-REAL n)
for r being Real holds the carrier of (Tball (p,r)) = Ball (p,r)