:: deftheorem Def5 defines Ciso TOPALG_5:def 5 :
for b₁ being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) holds
( b₁ = Ciso iff for n being Integer holds b₁ . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) );