let A be Ordinal; :: thesis: alef A is infinite
{} c= A by XBOOLE_1:2;
then omega c= alef A by CARD_1:23, CARD_1:46;
hence alef A is infinite ; :: thesis: verum