defpred S₁[ set ] means $1 in J;
defpred S₂[ set ] means $1 in I;
set X = { x where x is Element of R : ( S₂[x] & S₁[x] ) } ;
set Y = { x where x is Element of R : S₂[x] } ;
set Z = { x where x is Element of R : S₁[x] } ;
A1: { x where x is Element of R : S₂[x] } = I by DOMAIN_1:52;
{ x where x is Element of R : ( S₂[x] & S₁[x] ) } = { x where x is Element of R : S₂[x] } /\ { x where x is Element of R : S₁[x] } from DOMAIN_1:sch 10();
hence for b₁ being Subset of R holds
( b₁ = I /\ J iff b₁ = { x where x is Element of R : ( x in I & x in J ) } ) by A1, DOMAIN_1:52; :: thesis: verum