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:39, CARD_1:83;
hence ( not alef (succ 0 ) is limit_cardinal & not alef (succ 0 ) is finite ) ; :: thesis: verum