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 Th42;
nextcard (card X) = nextcard X by Def2, Th16;
hence nextcard X is finite by A1, Th38; :: thesis: verum