let M be Cardinal; :: thesis: M in exp (2,M)
( card (bool M) = exp (2,(card M)) & card M = M ) by CARD_2:31;
hence M in exp (2,M) by CARD_1:14; :: thesis: verum