let A be Ordinal; :: thesis: alef (succ A) = nextcard (alef A)
thus alef (succ A) = nextcard (union {(alef A)}) by Lm1
.= nextcard (alef A) by ZFMISC_1:25 ; :: thesis: verum