let A be Ordinal; :: thesis: ( A is_cofinal_with {} implies A = {} )
given psi being Ordinal-Sequence such that A1: ( dom psi = {} & rng psi c= A & psi is increasing & A = sup psi ) ; :: according to ORDINAL2:def 21 :: thesis: A = {}
thus A = sup {} by A1, RELAT_1:65
.= {} by Th26 ; :: thesis: verum