:: deftheorem defines Tball MFOLD_0:def 1 :
for n being Nat
for p being Point of (TOP-REAL n)
for r being Real holds Tball (p,r) = (TOP-REAL n) | (Ball (p,r));