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 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