let X, Y be set ; :: thesis: ( card X = card Y implies nextcard X = nextcard Y )
assume A1: card X = card Y ; :: thesis: nextcard X = nextcard Y
( card X in nextcard X & ( for N being Cardinal st card X in N holds
nextcard X c= N ) ) by Def3;
hence nextcard X = nextcard Y by A1, Def3; :: thesis: verum