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