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)
for x, y being set holds
( [x,y] in (X \/ Y) | R iff [x,y] in (X | R) \/ (Y | R) )

proof

let x, y be set ; :: thesis: ( [x,y] in (X \/ Y) | R iff [x,y] in (X | R) \/ (Y | R) )
( ( [x,y] in (X \/ Y) | R implies ( y in X \/ Y & [x,y] in R ) ) & ( y in X \/ Y & [x,y] in R implies [x,y] in (X \/ Y) | R ) & ( not y in X \/ Y or y in X or y in Y ) & ( ( y in X or y in Y ) implies y in X \/ Y ) & ( not [x,y] in (X | R) \/ (Y | R) or [x,y] in X | R or [x,y] in Y | R ) & ( ( [x,y] in X | R or [x,y] in Y | R ) implies [x,y] in (X | R) \/ (Y | R) ) & ( [x,y] in X | R implies ( y in X & [x,y] in R ) ) & ( y in X & [x,y] in R implies [x,y] in X | R ) & ( [x,y] in Y | R implies ( y in Y & [x,y] in R ) ) & ( y in Y & [x,y] in R implies [x,y] in Y | R ) ) by Def12, XBOOLE_0:def 3;
hence ( [x,y] in (X \/ Y) | R iff [x,y] in (X | R) \/ (Y | R) ) ; :: thesis: verum

end;

hence (X \/ Y) | R = (X | R) \/ (Y | R) by Def2; :: thesis: verum