card M = M by CARD_1:def 5;
then exp (2,M) = card (bool M) by CARD_2:44;
hence not exp (2,M) is finite ; :: thesis: verum