theorem Th26: :: ARYTM_3:26

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