theorem :: ORDINAL2:31

for A being Ordinal holds A +^ 1 = succ A