theorem Th20: :: ARYTM_3:20

for a, b being natural Ordinal holds
( a,b are_coprime iff a hcf b = 1 )