let R be non empty associative multLoopStr ; :: thesis: for a, b, c being Element of st a divides b & b divides c holds
a divides c
let A, B, C be Element of ; :: thesis: ( A divides B & B divides C implies A divides C )

now

assume that
A1: A divides B and
A2: B divides C ; :: thesis: ( A divides B & B divides C implies A divides C )
consider D being Element of such that
A3: A * D = B by A1, Def1;
consider E being Element of such that
A4: B * E = C by A2, Def1;
A * (D * E) = C by A3, A4, GROUP_1:def 4;
hence ( A divides B & B divides C implies A divides C ) by Def1; :: thesis: verum

end;

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