let X be set ; :: thesis: card {} in nextcard X
( card {} c= card X & card X in nextcard X ) by Def6;
hence card {} in nextcard X by ORDINAL1:22; :: thesis: verum