theorem :: RELSET_2:33
for A, B being set
for X being Subset of A
for R1, R2 being Subset of [:A,B:] holds (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)