:: deftheorem defines Tdisk BROUWER:def 2 :
for n being Nat
for x being Point of (TOP-REAL n)
for r being Real holds Tdisk (x,r) = (TOP-REAL n) | (cl_Ball (x,r));