:: deftheorem Def5 defines FundamentalGroup TOPALG_1:def 5 :
for X being non empty TopSpace
for a being Point of X
for b₃ being strict multMagma holds
( b₃ = FundamentalGroup (X,a) iff ( the carrier of b₃ = Class (EqRel (X,a)) & ( for x, y being Element of b₃ ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b₃ . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) ) );