theorem Th36: :: GR_FREE0:35

for I being non empty set
for G being Group-like multMagma-Family of I
for p, q being FinSequence of FreeAtoms G holds
( not ReductionRel G reduces p,q or p = q or len q < len p )