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