for n being non zero Nat
for x, y being Nat st x in NatDivisors n & y in NatDivisors n holds
x lcm y in NatDivisors n