let A be Ordinal; :: thesis: A in nextcard A
assume not A in nextcard A ; :: thesis: contradiction
then A1: card (nextcard A) c= card A by Th27, ORDINAL1:16;
A, card A are_equipotent by Def5;
then A2: nextcard (card A) = nextcard A by Th35;
XX: card (card A) in nextcard (card A) by Def6;
card (nextcard A) = nextcard A by Def5;
hence contradiction by A1, A2, XX, ORDINAL1:5; :: thesis: verum