let N be Cardinal; :: thesis: nextcard N c= exp (2,N)
card N in exp (2,N) by CARD_5:14;
hence nextcard N c= exp (2,N) by CARD_1:def 3; :: thesis: verum