let X, Y be set ; :: thesis: for R being Relation holds R | (X /\ Y) = (R | X) /\ (R | Y)
let R be Relation; :: thesis: R | (X /\ Y) = (R | X) /\ (R | Y)
let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in R | (X /\ Y) iff [x,b] in (R | X) /\ (R | Y) )
let y be object ; :: thesis: ( [x,y] in R | (X /\ Y) iff [x,y] in (R | X) /\ (R | Y) )

hereby :: thesis: ( [x,y] in (R | X) /\ (R | Y) implies [x,y] in R | (X /\ Y) )

assume A1: [x,y] in R | (X /\ Y) ; :: thesis: [x,y] in (R | X) /\ (R | Y)
then A2: x in X /\ Y by Def9;
A3: [x,y] in R by A1, Def9;
x in Y by A2, XBOOLE_0:def 4;
then A4: [x,y] in R | Y by A3, Def9;
x in X by A2, XBOOLE_0:def 4;
then [x,y] in R | X by A3, Def9;
hence [x,y] in (R | X) /\ (R | Y) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

assume A5: [x,y] in (R | X) /\ (R | Y) ; :: thesis: [x,y] in R | (X /\ Y)
then [x,y] in R | Y by XBOOLE_0:def 4;
then A6: x in Y by Def9;
A7: [x,y] in R | X by A5, XBOOLE_0:def 4;
then x in X by Def9;
then A8: x in X /\ Y by A6, XBOOLE_0:def 4;
[x,y] in R by A7, Def9;
hence [x,y] in R | (X /\ Y) by A8, Def9; :: thesis: verum