theorem Th30: :: ORDINAL2:30

for A being Ordinal holds 0 +^ A = A