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