for A being Ordinal holds sup {A} = succ A