for A being Ordinal holds succ A is_cofinal_with 1