theorem :: INT_2:17

for a, b being Integer holds a lcm b is Element of NAT by ORDINAL1:def 12;