let A be Ordinal; ( A is_cofinal_with {} implies A = {} )
given psi being Ordinal-Sequence such that A1:
dom psi = {}
and
rng psi c= A
and
psi is increasing
and
A2:
A = sup psi
; ORDINAL2:def 17 A = {}
thus A =
sup {}
by A1, A2, RELAT_1:42
.=
{}
by Th26
; verum