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