theorem Th4: :: INT_2:4

for a, b being Integer holds
( ( a = 0 or b = 0 ) iff a lcm b = 0 )