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:31;
then exp (2,N) is finite ;
hence exp (2,N) in omega by CARD_1:61; :: thesis: verum