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:27;
then A4: card y c= card n by XBOOLE_1:1;
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