let X, Y be set ; :: thesis: for R being Relation holds (R |_2 X) |_2 Y = R |_2 (X /\ Y)
let R be Relation; :: thesis: (R |_2 X) |_2 Y = R |_2 (X /\ Y)
thus (R |_2 X) |_2 Y = R /\ ([:X,X:] /\ [:Y,Y:]) by XBOOLE_1:16
.= R |_2 (X /\ Y) by ZFMISC_1:100 ; :: thesis: verum