let X be set ; :: thesis: nextcard (card X) = nextcard X
( card (card X) in nextcard X & ( for M being Cardinal st card (card X) in M holds
nextcard X c= M ) ) by CARD_1:def 6;
hence nextcard (card X) = nextcard X by CARD_1:def 6; :: thesis: verum