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 set ; :: 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 set such that
A8: [x,y] in R and
A9: y in X \/ Y by Def14;
( y in X or y in Y ) by A9, XBOOLE_0:def 3;
then ( x in R " X or x in R " Y ) by A8, Def14;
hence x in (R " X) \/ (R " Y) by XBOOLE_0:def 3; :: thesis: verum

end;

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

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

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

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

end;

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

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

end;

end;