let X be set ; :: thesis: ( X is finite implies nextcard X is finite )
assume X is finite ; :: thesis: nextcard X is finite
then reconsider X = X as finite set ;
card X = card (card X) ;
then A1: card (succ (card X)) = nextcard (card X) by Th76;
X, card X are_equipotent by Def5;
then nextcard (card X) = nextcard X by Th35;
hence nextcard X is finite by A1, Th69; :: thesis: verum