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:26;
A, card A are_equipotent by Def5;
then A2: nextcard (card A) = nextcard A by Th35;
card (nextcard A) = nextcard A by Def5;
hence contradiction by A1, A2, Th32, ORDINAL1:7; :: thesis: verum