let X, Y be set ; ( card X = card Y iff nextcard X = nextcard Y )
thus
( card X = card Y implies nextcard X = nextcard Y )
by CARD_1:16; ( nextcard X = nextcard Y implies card X = card Y )
assume that
A1:
nextcard X = nextcard Y
and
A2:
card X <> card Y
; contradiction
( card X in card Y or card Y in card X )
by A2, ORDINAL1:14;
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 3;
hence
contradiction
by A1, ORDINAL1:12; verum