A1: {} c= Y by XBOOLE_1:2;
( 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