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