:: deftheorem defines Tcircle TOPREALB:def 6 :
for n being Nat
for x being Point of (TOP-REAL n)
for r being Real holds Tcircle (x,r) = (TOP-REAL n) | (Sphere (x,r));