theorem :: ZFREFLE1:24

for A, B being Ordinal st A is_cofinal_with succ B holds
ex C being Ordinal st A = succ C