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