A1: {} c= Y ;
( card {} c= card n & {} in X ) by SETFAM_1:def 8;
then {} in the_subsets_with_limited_card (n,X,Y) by A1, Def2;
hence the_subsets_with_limited_card (n,X,Y) is with_empty_element ; :: thesis: verum