for n, m being Element of NAT st 1 <= n & 1 <= m holds
ex m0, n0 being Element of NAT st
( n lcm m = n0 * m0 & n0 gcd m0 = 1 & n0 divides n & m0 divides m & n0 <> 0 & m0 <> 0 )