defpred S₁[ set ] means $1 in I;
defpred S₂[ set ] means $1 in J;
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] & 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();
( { x where x is Element of R : S₁[x] } = I & { x where x is Element of R : S₂[x] } = J ) by DOMAIN_1:52;
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; :: thesis: verum