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

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