:: deftheorem defines Ball TOPREAL9:def 1 :
for n being Nat
for x being Point of (TOP-REAL n)
for r being Real holds Ball (x,r) = { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } ;