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 Th10, ORDINAL1:16;
A2: nextcard (card A) = nextcard A by Def2, Th16;
A3: card (card A) in nextcard (card A) by Def3;
thus contradiction by A1, A2, A3, ORDINAL1:5; :: thesis: verum