let x be set ; :: according to CLASSES1:def 1 :: thesis: for b₁ being set holds
( not x in the_subsets_with_limited_card (n,X,Y) or not b₁ c= x or b₁ in the_subsets_with_limited_card (n,X,Y) )
let y be set ; :: thesis: ( not x in the_subsets_with_limited_card (n,X,Y) or not y c= x or y in the_subsets_with_limited_card (n,X,Y) )
assume that
A1: x in the_subsets_with_limited_card (n,X,Y) and
A2: y c= x ; :: thesis: y in the_subsets_with_limited_card (n,X,Y)
x in X by A1, Def2;
then A3: y in X by A2, CLASSES1:def 1;
( card x c= card n & card y c= card x ) by A1, A2, Def2, CARD_1:11;
then A4: card y c= card n ;
y c= Y by A1, A2, XBOOLE_1:1;
hence y in the_subsets_with_limited_card (n,X,Y) by A3, A4, Def2; :: thesis: verum