let X, Y be set ; :: thesis: ( X,Y are_equipotent implies nextcard X = nextcard Y )
assume X,Y are_equipotent ; :: thesis: nextcard X = nextcard Y
then card X = card Y by Th4;
hence nextcard X = nextcard Y by Th15; :: thesis: verum