theorem Th27: :: ORDINAL2:27

for A being Ordinal holds A +^ 0 = A