let A, B be Ordinal; :: thesis: ( A is_cofinal_with succ B implies ex C being Ordinal st A = succ C )
given psi being Ordinal-Sequence such that A1: dom psi = succ B and
A2: rng psi c= A and
A3: psi is increasing and
A4: A = sup psi ; :: according to ORDINAL2:def 17 :: thesis: ex C being Ordinal st A = succ C
reconsider C = psi . B as Ordinal ;
take C ; :: thesis: A = succ C
thus A c= succ C :: according to XBOOLE_0:def 10 :: thesis: succ C c= A

proof

let a be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not a in A or a in succ C )
assume a in A ; :: thesis: a in succ C
then consider b being Ordinal such that
A5: b in rng psi and
A6: a c= b by A4, ORDINAL2:21;
consider e being object such that
A7: e in succ B and
A8: b = psi . e by A1, A5, FUNCT_1:def 3;
reconsider e = e as Ordinal by A7;
e c= B by A7, ORDINAL1:22;
then b c= C by A1, A3, A8, ORDINAL1:6, ORDINAL4:9;
then b in succ C by ORDINAL1:22;
hence a in succ C by A6, ORDINAL1:12; :: thesis: verum

end;

B in succ B by ORDINAL1:6;
then C in rng psi by A1, FUNCT_1:def 3;
hence succ C c= A by A2, ORDINAL1:21; :: thesis: verum