for A being Ordinal
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