let i, j, h be Nat; :: thesis: ( i divides j & j divides h implies i divides h )
assume that
A1: i divides j and
A2: j divides h ; :: thesis: i divides h
A3: j = i * (j div i) by A1, Th3;
h = j * (h div j) by A2, Th3;
then h = i * ((j div i) * (h div j)) by A3;
hence i divides h by Def3; :: thesis: verum