for r being non negative Real
for n being non zero Nat
for p being Point of (Tcircle ((0. (TOP-REAL n)),r)) holds - p is Point of (Tcircle ((0. (TOP-REAL n)),r))