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;
consider l being Integer such that
A4: c = b * l by A2;
c = a * (k * l) by A3, A4;
hence a divides c ; :: thesis: verum