set SS = { A where A is Subset of Y : ( A in X & card A c= n ) } ;
{ A where A is Subset of Y : ( A in X & card A c= n ) } c= bool Y

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of Y : ( A in X & card A c= n ) } or x in bool Y )
assume x in { A where A is Subset of Y : ( A in X & card A c= n ) } ; :: thesis: x in bool Y
then ex A being Subset of Y st
( x = A & A in X & card A c= n ) ;
hence x in bool Y ; :: thesis: verum

end;

then reconsider SS = { A where A is Subset of Y : ( A in X & card A c= n ) } as Subset-Family of Y ;
take SS ; :: thesis: for A being Subset of Y holds
( A in SS iff ( A in X & card A c= n ) )
let A be Subset of Y; :: thesis: ( A in SS iff ( A in X & card A c= n ) )

hereby :: thesis: ( A in X & card A c= n implies A in SS )

assume A in SS ; :: thesis: ( A in X & card A c= n )
then ex B being Subset of Y st
( B = A & B in X & card B c= n ) ;
hence ( A in X & card A c= n ) ; :: thesis: verum

end;

assume ( A in X & card A c= n ) ; :: thesis: A in SS
hence A in SS ; :: thesis: verum