let A, B be Ordinal; :: thesis: ( A is_cofinal_with B implies B c= A )
given psi being Ordinal-Sequence such that A1: dom psi = B and
A2: rng psi c= A and
A3: psi is increasing and
A = sup psi ; :: according to ORDINAL2:def 17 :: thesis: B c= A
let C be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not C in B or C in A )
assume C in B ; :: thesis: C in A
then ( C c= psi . C & psi . C in rng psi ) by A1, A3, FUNCT_1:def 3, ORDINAL4:10;
hence C in A by A2, ORDINAL1:12; :: thesis: verum