let A be set ; :: according to FINSET_1:def 6 :: thesis: ( not A in the_subsets_with_limited_card (n,X,Y) or A is finite )
assume A in the_subsets_with_limited_card (n,X,Y) ; :: thesis: A is finite
then card A c= card n by Def2;
hence A is finite ; :: thesis: verum