let A be set ; :: according to MATROID0:def 5 :: 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