:: deftheorem Def3 defines ReductionRel GR_FREE0:def 3 :
for I being non empty set
for G being Group-like multMagma-Family of I
for b₃ being Relation of ((FreeAtoms G) *+^+<0>) holds
( b₃ = ReductionRel G iff for p, q being FinSequence of FreeAtoms G holds
( [p,q] in b₃ iff ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I st
( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex g, h being Element of (G . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) );