:: deftheorem defines Tunit_circle TOPREALB:def 7 :
for n being Nat holds Tunit_circle n = Tcircle ((0. (TOP-REAL n)),1);