let N be Cardinal; :: according to CARD_FIL:def 14 :: thesis: ( N in omega implies exp 2,N in omega )
assume N in omega ; :: thesis: exp 2,N in omega
then N is finite ;
then card (bool N) is finite ;
then exp 2,(card N) is finite by CARD_2:44;
then exp 2,N is finite by CARD_1:def 5;
hence exp 2,N in omega by CARD_1:103; :: thesis: verum