let a, b, c be Integer; :: thesis: ( a divides b & b divides c implies a divides c )
assume that
A1: a divides b and
A2: b divides c ; :: thesis: a divides c
consider k being Integer such that
A3: b = a * k by A1, INT_1:def 9;
consider l being Integer such that
A4: c = b * l by A2, INT_1:def 9;
c = a * (k * l) by A3, A4;
hence a divides c by INT_1:def 9; :: thesis: verum