theorem Th4: :: GCD_1:4

for R being non empty associative multLoopStr
for a, b, c being Element of R st a is_associated_to b & b is_associated_to c holds
a is_associated_to c by Th2;