let M be Cardinal; :: thesis: M in exp 2,M
( card (bool M) = exp 2,(card M) & card M = M ) by CARD_1:def 5, CARD_2:44;
hence M in exp 2,M by CARD_1:30; :: thesis: verum