theorem Th23: :: ARYTM_3:23

for a, b being natural Ordinal st a,b are_coprime holds
RED (a,b) = a