theorem Th13: :: ARYTM_3:13

for m, n being natural Ordinal st n <> {} holds
(m *^ n) div^ (m lcm n) divides m