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

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