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