let S1, S2 be Subset-Family of Y; :: thesis: ( ( for A being Subset of Y holds
( A in S1 iff ( A in X & card A c= n ) ) ) & ( for A being Subset of Y holds
( A in S2 iff ( A in X & card A c= n ) ) ) implies S1 = S2 )
assume that
A1: for A being Subset of Y holds
( A in S1 iff ( A in X & card A c= n ) ) and
A2: for A being Subset of Y holds
( A in S2 iff ( A in X & card A c= n ) ) ; :: thesis: S1 = S2
thus S1 c= S2 :: according to XBOOLE_0:def 10 :: thesis: S2 c= S1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S1 or x in S2 )
reconsider xx = x as set by TARSKI:1;
assume A3: x in S1 ; :: thesis: x in S2
then ( x in X & card xx c= n ) by A1;
hence x in S2 by A2, A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S2 or x in S1 )
reconsider xx = x as set by TARSKI:1;
assume A4: x in S2 ; :: thesis: x in S1
then ( x in X & card xx c= n ) by A2;
hence x in S1 by A1, A4; :: thesis: verum