theorem :: ORDINAL3:73

for A being Ordinal holds succ A is_cofinal_with 1