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