let X, Y be set ; :: thesis: ( card X = card Y iff nextcard X = nextcard Y )
thus ( card X = card Y implies nextcard X = nextcard Y ) by CARD_1:34; :: thesis: ( nextcard X = nextcard Y implies card X = card Y )
assume A1: ( nextcard X = nextcard Y & card X <> card Y ) ; :: thesis: contradiction
then ( card X in card Y or card Y in card X ) by ORDINAL1:24;
then ( ( nextcard X c= card Y & card Y in nextcard Y ) or ( nextcard Y c= card X & card X in nextcard X ) ) by CARD_1:def 6;
hence contradiction by A1, ORDINAL1:22; :: thesis: verum