:: deftheorem defines is_cofinal_with ORDINAL2:def 17 :
for A, B being Ordinal holds
( A is_cofinal_with B iff ex xi being Ordinal-Sequence st
( dom xi = B & rng xi c= A & xi is increasing & A = sup xi ) );