defpred S1[ set ] means $1 in J; defpred S2[ set ] means $1 in I; set X = { x where x is Element of R : ( S2[x] & S1[x] ) } ; set Y = { x where x is Element of R : S2[x] } ; set Z = { x where x is Element of R : S1[x] } ; A1:
{ x where x is Element of R : S2[x] } = I
byDOMAIN_1:22; { x where x is Element of R : ( S2[x] & S1[x] ) } = { x where x is Element of R : S2[x] } /\ { x where x is Element of R : S1[x] } fromDOMAIN_1:sch 10(); hence
for b1 being Subset of R holds ( b1= I /\ J iff b1= { x where x is Element of R : ( x in I & x in J ) } )
byA1, DOMAIN_1:22; :: thesis: verum