let X be set ; :: thesis: for P, Q being Relation holds (P \/ Q) | X = (P | X) \/ (Q | X)
let P, Q be Relation; :: thesis: (P \/ Q) | X = (P | X) \/ (Q | X)
set R1 = P | X;
set R2 = Q | X;
set R = P \/ Q;
set LH = (P \/ Q) | X;
set RH = (P | X) \/ (Q | X);
( (P null Q) | X c= (P \/ Q) | X & (Q null P) | X c= (P \/ Q) | X ) by RELAT_1:76;
then A1: (P | X) \/ (Q | X) c= (P \/ Q) | X by XBOOLE_1:8;

now :: thesis: for z being object st z in (P \/ Q) | X holds
z in (P | X) \/ (Q | X)

let z be object ; :: thesis: ( z in (P \/ Q) | X implies z in (P | X) \/ (Q | X) )
assume A2: z in (P \/ Q) | X ; :: thesis: z in (P | X) \/ (Q | X)
then consider x, y being object such that
A3: z = [x,y] by RELAT_1:def 1;
A4: ( x in X & [x,y] in P \/ Q ) by RELAT_1:def 11, A2, A3;
( ( x in X & [x,y] in P ) or ( x in X & [x,y] in Q ) ) by A4, XBOOLE_0:def 3;
then ( [x,y] in P | X or [x,y] in Q | X ) by RELAT_1:def 11;
hence z in (P | X) \/ (Q | X) by XBOOLE_0:def 3, A3; :: thesis: verum

end;

then (P \/ Q) | X c= (P | X) \/ (Q | X) ;
hence (P \/ Q) | X = (P | X) \/ (Q | X) by A1; :: thesis: verum