let a, b, c, d be Nat; :: thesis: ( a divides c & b divides d implies a * b divides c * d )
given x being Nat such that A1: c = a * x ; :: according to NAT_D:def 3 :: thesis: ( not b divides d or a * b divides c * d )
given y being Nat such that A2: d = b * y ; :: according to NAT_D:def 3 :: thesis: a * b divides c * d
take x * y ; :: according to NAT_D:def 3 :: thesis: c * d = (a * b) * (x * y)
thus c * d = (a * b) * (x * y) by A1, A2; :: thesis: verum