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

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