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)
thus R " (X \/ Y) c= (R " X) \/ (R " Y) :: according to XBOOLE_0:def 10 :: thesis: (R " X) \/ (R " Y) c= R " (X \/ Y)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R " (X \/ Y) or x in (R " X) \/ (R " Y) )
assume x in R " (X \/ Y) ; :: thesis: x in (R " X) \/ (R " Y)
then consider y being object such that
A1: [x,y] in R and
A2: y in X \/ Y by Def12;
( y in X or y in Y ) by A2, XBOOLE_0:def 3;
then ( x in R " X or x in R " Y ) by A1, Def12;
hence x in (R " X) \/ (R " Y) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R " X) \/ (R " Y) or x in R " (X \/ Y) )
assume A3: x in (R " X) \/ (R " Y) ; :: thesis: x in R " (X \/ Y)

per cases ( x in R " Y or x in R " X ) by A3, XBOOLE_0:def 3;

suppose x in R " Y ; :: thesis: x in R " (X \/ Y)

then consider y being object such that
A4: [x,y] in R and
A5: y in Y by Def12;
y in X \/ Y by A5, XBOOLE_0:def 3;
hence x in R " (X \/ Y) by A4, Def12; :: thesis: verum

end;

suppose x in R " X ; :: thesis: x in R " (X \/ Y)

then consider y being object such that
A6: [x,y] in R and
A7: y in X by Def12;
y in X \/ Y by A7, XBOOLE_0:def 3;
hence x in R " (X \/ Y) by A6, Def12; :: thesis: verum

end;

end;