for n being non zero Nat
for r being positive Real
for x being Point of (TOP-REAL n) st n >= 3 holds
Tcircle (x,r) is having_trivial_Fundamental_Group