theorem Th99: :: ORDINAL7:86

for a, b being Ordinal holds a c= a (+) b