:: deftheorem Def1 defines ball MFOLD_1:def 1 :
for n being Nat
for S being Subset of (TOP-REAL n) holds
( S is ball iff ex p being Point of (TOP-REAL n) ex r being Real st S = Ball (p,r) );