take alef (succ 0) ; :: thesis: ( not alef (succ 0) is limit_cardinal & alef (succ 0) is infinite )
alef (succ 0) = nextcard omega by CARD_1:19, CARD_1:46;
hence ( not alef (succ 0) is limit_cardinal & alef (succ 0) is infinite ) ; :: thesis: verum