theorem Th27: :: ARYTM_3:27

for a being natural Ordinal st a <> {} holds
RED (a,a) = 1