let N be Cardinal; :: thesis: nextcard N c= exp (2,N)
card N = N by CARD_1:def 5;
then card N in exp (2,N) by CARD_5:23;
hence nextcard N c= exp (2,N) by CARD_1:def 6; :: thesis: verum