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)

now

let x, y be set ; :: thesis: ( [x,y] in R | (X \/ Y) iff [x,y] in (R | X) \/ (R | Y) )

A1: now

A2: now

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

end;

A5: now

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

end;

assume [x,y] in (R | X) \/ (R | Y) ; :: thesis: [x,y] in R | (X \/ Y)
hence [x,y] in R | (X \/ Y) by A5, A2, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume A8: [x,y] in R | (X \/ Y) ; :: thesis: [x,y] in (R | X) \/ (R | Y)
then x in X \/ Y by Def11;
then A9: ( x in X or x in Y ) by XBOOLE_0:def 3;
[x,y] in R by A8, Def11;
then ( [x,y] in R | X or [x,y] in R | Y ) by A9, Def11;
hence [x,y] in (R | X) \/ (R | Y) by XBOOLE_0:def 3; :: thesis: verum

end;

hence ( [x,y] in R | (X \/ Y) iff [x,y] in (R | X) \/ (R | Y) ) by A1; :: thesis: verum

end;

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