theorem Th24: :: ARYTM_3:24

for a being natural Ordinal holds
( RED (a,1) = a & RED (1,a) = 1 )