let A be Ordinal; :: thesis: for psi being Ordinal-Sequence st dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A is_limes_of psi holds
A is_cofinal_with dom psi
let psi be Ordinal-Sequence; :: thesis: ( dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A is_limes_of psi implies A is_cofinal_with dom psi )
assume that
A1: ( dom psi <> {} & dom psi is limit_ordinal ) and
A2: psi is increasing and
A3: A is_limes_of psi ; :: thesis: A is_cofinal_with dom psi
take psi ; :: according to ORDINAL2:def 17 :: thesis: ( dom psi = dom psi & rng psi c= A & psi is increasing & A = sup psi )
thus dom psi = dom psi ; :: thesis: ( rng psi c= A & psi is increasing & A = sup psi )
( sup psi = lim psi & A = lim psi ) by A1, A2, A3, ORDINAL2:def 10, ORDINAL4:8;
hence ( rng psi c= A & psi is increasing & A = sup psi ) by A2, ORDINAL2:49; :: thesis: verum