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)
let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in R | (X \/ Y) iff [x,b] in (R | X) \/ (R | Y) )
let y be object ; :: thesis: ( [x,y] in R | (X \/ Y) iff [x,y] in (R | X) \/ (R | Y) )
hereby :: thesis: ( [x,y] in (R | X) \/ (R | Y) implies [x,y] in R | (X \/ Y) )
assume A1: [x,y] in R | (X \/ Y) ; :: thesis: [x,y] in (R | X) \/ (R | Y)
then x in X \/ Y by Def9;
then A2: ( x in X or x in Y ) by XBOOLE_0:def 3;
[x,y] in R by A1, Def9;
then ( [x,y] in R | X or [x,y] in R | Y ) by A2, Def9;
hence [x,y] in (R | X) \/ (R | Y) by XBOOLE_0:def 3; :: thesis: verum
end;
assume A3: [x,y] in (R | X) \/ (R | Y) ; :: thesis: [x,y] in R | (X \/ Y)
per cases ( [x,y] in R | Y or [x,y] in R | X ) by A3, XBOOLE_0:def 3;
suppose A4: [x,y] in R | Y ; :: thesis: [x,y] in R | (X \/ Y)
then x in Y by Def9;
then A5: x in X \/ Y by XBOOLE_0:def 3;
[x,y] in R by A4, Def9;
hence [x,y] in R | (X \/ Y) by A5, Def9; :: thesis: verum
end;
suppose A6: [x,y] in R | X ; :: thesis: [x,y] in R | (X \/ Y)
then x in X by Def9;
then A7: x in X \/ Y by XBOOLE_0:def 3;
[x,y] in R by A6, Def9;
hence [x,y] in R | (X \/ Y) by A7, Def9; :: thesis: verum
end;
end;