let A, B be Ordinal; :: thesis: ( A is_cofinal_with B implies ( A is limit_ordinal iff B is limit_ordinal ) )
given psi being Ordinal-Sequence such that A1: dom psi = B and
A2: rng psi c= A and
A3: psi is increasing and
A4: A = sup psi ; :: according to ORDINAL2:def 17 :: thesis: ( A is limit_ordinal iff B is limit_ordinal )
thus ( A is limit_ordinal implies B is limit_ordinal ) :: thesis: ( B is limit_ordinal implies A is limit_ordinal )

proof

assume A5: A is limit_ordinal ; :: thesis: B is limit_ordinal

now :: thesis: for C being Ordinal st C in B holds
succ C in B

let C be Ordinal; :: thesis: ( C in B implies succ C in B )
reconsider c = psi . C as Ordinal ;
assume A6: C in B ; :: thesis: succ C in B
then psi . C in rng psi by A1, FUNCT_1:def 3;
then succ c in A by A2, A5, ORDINAL1:28;
then consider b being Ordinal such that
A7: b in rng psi and
A8: succ c c= b by A4, ORDINAL2:21;
consider e being object such that
A9: e in B and
A10: b = psi . e by A1, A7, FUNCT_1:def 3;
reconsider e = e as Ordinal by A9;
c in succ c by ORDINAL1:6;
then not e c= C by A1, A3, A6, A8, A10, Th9, ORDINAL1:5;
then C in e by ORDINAL1:16;
then succ C c= e by ORDINAL1:21;
hence succ C in B by A9, ORDINAL1:12; :: thesis: verum

end;

hence B is limit_ordinal by ORDINAL1:28; :: thesis: verum

end;

thus ( B is limit_ordinal implies A is limit_ordinal ) by A1, A3, A4, Th16; :: thesis: verum