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