theorem Th15: :: ARYTM_3:15

for a, b being natural Ordinal st a hcf b = {} holds
a = {}