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 Th11, ORDINAL1:16;
A, card A are_equipotent by Def2;
then A2: nextcard (card A) = nextcard A by Th17;
A3: card (card A) in nextcard (card A) by Def3;
card (nextcard A) = nextcard A by Def2;
hence contradiction by A1, A2, A3, ORDINAL1:5; :: thesis: verum