let x be set ; CLASSES1:def 1 for b1 being set holds
( not x in the_subsets_with_limited_card (n,X,Y) or not b1 c= x or b1 in the_subsets_with_limited_card (n,X,Y) )
let y be set ; ( 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
; 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; verum