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 & rng psi c= A & psi is increasing & A = sup psi ) ; :: according to ORDINAL2:def 21 :: 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 A2: A is limit_ordinal ; :: thesis: B is limit_ordinal

now

let C be Ordinal; :: thesis: ( C in B implies succ C in B )
assume A3: C in B ; :: thesis: succ C in B
then A4: psi . C in rng psi by A1, FUNCT_1:def 5;
reconsider c = psi . C as Ordinal ;
( succ c in A & A = sup (rng psi) ) by A1, A2, A4, ORDINAL1:41;
then consider b being Ordinal such that
A5: ( b in rng psi & succ c c= b ) by ORDINAL2:29;
consider e being set such that
A6: ( e in B & b = psi . e ) by A1, A5, FUNCT_1:def 5;
reconsider e = e as Ordinal by A6;
c in succ c by ORDINAL1:10;
then not e c= C by A1, A3, A5, A6, Th9, ORDINAL1:7;
then C in e by ORDINAL1:26;
then succ C c= e by ORDINAL1:33;
hence succ C in B by A6, ORDINAL1:22; :: thesis: verum

end;

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

end;

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