theorem Th19: :: ARYTM_3:19

for a, b being natural Ordinal st ( a <> {} or b <> {} ) holds
a div^ (a hcf b),b div^ (a hcf b) are_coprime