let X, Y be set ; :: thesis: for R being Relation holds (X /\ Y) | R = (X | R) /\ (Y | R)
let R be Relation; :: thesis: (X /\ Y) | R = (X | R) /\ (Y | R)
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [x,b] in (X /\ Y) | R iff [x,b] in (X | R) /\ (Y | R) )
let y be set ; :: thesis: ( [x,y] in (X /\ Y) | R iff [x,y] in (X | R) /\ (Y | R) )
A1: ( y in X /\ Y iff ( y in X & y in Y ) ) by XBOOLE_0:def 4;
A2: ( [x,y] in (X | R) /\ (Y | R) iff ( [x,y] in X | R & [x,y] in Y | R ) ) by XBOOLE_0:def 4;
( [x,y] in (X /\ Y) | R iff ( y in X /\ Y & [x,y] in R ) ) by Def12;
hence ( [x,y] in (X /\ Y) | R iff [x,y] in (X | R) /\ (Y | R) ) by A1, A2, Def12; :: thesis: verum