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