let A be Ordinal; :: thesis: A in nextcard A
assume not A in nextcard A ; :: thesis: contradiction
then ( nextcard A c= A & A, card A are_equipotent ) by Def5, ORDINAL1:26;
then ( card (nextcard A) c= card A & card (nextcard A) = nextcard A & nextcard (card A) = nextcard A & card A in nextcard (card A) ) by Def5, Th27, Th32, Th35;
hence contradiction by ORDINAL1:7; :: thesis: verum