let n, m be Nat; :: thesis: ( m > 0 & n > 0 implies m lcm n > 0 )
assume that
A1: m > 0 and
A2: n > 0 and
A3: m lcm n <= 0 ; :: thesis: contradiction
A4: m lcm n divides m * n by Th47;
( m lcm n = 0 or m lcm n < 0 ) by A3;
then ex r being Nat st m * n = 0 * r by A4, NAT_D:def 3;
hence contradiction by A1, A2; :: thesis: verum