let R be non empty associative multLoopStr ; :: thesis: 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
let A, B, C be Element of R; :: thesis: ( A is_associated_to B & B is_associated_to C implies A is_associated_to C )

now

assume A1: ( A is_associated_to B & B is_associated_to C ) ; :: thesis: ( A is_associated_to B & B is_associated_to C implies A is_associated_to C )
then ( B divides A & C divides B ) by Def3;
then A2: C divides A by Th2;
( A divides B & B divides C ) by A1, Def3;
then A divides C by Th2;
hence ( A is_associated_to B & B is_associated_to C implies A is_associated_to C ) by A2, Def3; :: thesis: verum

end;

hence ( A is_associated_to B & B is_associated_to C implies A is_associated_to C ) ; :: thesis: verum