let n, m be Nat; :: thesis: n gcd m divides n lcm m
A1: n divides n lcm m by NAT_D:def 4;
n gcd m divides n by NAT_D:def 5;
hence n gcd m divides n lcm m by A1, NAT_D:4; :: thesis: verum