for A being Ordinal holds succ A is_cofinal_with 1 by ORDINAL3:73;