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

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