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 3;
hence nextcard (card X) = nextcard X by CARD_1:def 3; :: thesis: verum