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