set IT = { A where A is Subset of U : ( X c= A & A c= Y ) } ;
{ A where A is Subset of U : ( X c= A & A c= Y ) } c= bool U

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of U : ( X c= A & A c= Y ) } or x in bool U )
assume x in { A where A is Subset of U : ( X c= A & A c= Y ) } ; :: thesis: x in bool U
then x in { A where A is Subset of U : ( X c= A & A c= Y ) } ;
then consider B being Subset of U such that
A1: ( x = B & X c= B & B c= Y ) ;
thus x in bool U by A1; :: thesis: verum

end;

then { A where A is Subset of U : ( X c= A & A c= Y ) } is Subset-Family of U ;
hence { A where A is Subset of U : ( X c= A & A c= Y ) } is Subset-Family of U ; :: thesis: verum