for n being Element of NAT
for r being Real
for x being Point of (TOP-REAL n) holds the carrier of (Tcircle (x,r)) = Sphere (x,r)