theorem Th90: :: ORDINAL7:77

for a being Ordinal holds a (+) 1 = succ a