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