theorem :: ORDINAL2:23

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