let A be Ordinal; :: thesis: not alef A is finite
{} c= A by XBOOLE_1:2;
then omega c= alef A by CARD_1:43, CARD_1:83;
hence not alef A is finite by CARD_3:102; :: thesis: verum