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

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

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

proof

then
{ A where A is Subset of U : ( X c= A & A c= Y ) } is Subset-Family of U
;
let x be object ; :: 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;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

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