let X, Y be set ; for R being Relation holds R | (X /\ Y) = (R | X) /\ (R | Y)
let R be Relation; R | (X /\ Y) = (R | X) /\ (R | Y)
let x be object ; RELAT_1:def 2 for b being object holds
( [x,b] in R | (X /\ Y) iff [x,b] in (R | X) /\ (R | Y) )
let y be object ; ( [x,y] in R | (X /\ Y) iff [x,y] in (R | X) /\ (R | Y) )
hereby ( [x,y] in (R | X) /\ (R | Y) implies [x,y] in R | (X /\ Y) )
assume A1:
[x,y] in R | (X /\ Y)
;
[x,y] in (R | X) /\ (R | Y)then A2:
x in X /\ Y
by Def9;
A3:
[x,y] in R
by A1, Def9;
x in Y
by A2, XBOOLE_0:def 4;
then A4:
[x,y] in R | Y
by A3, Def9;
x in X
by A2, XBOOLE_0:def 4;
then
[x,y] in R | X
by A3, Def9;
hence
[x,y] in (R | X) /\ (R | Y)
by A4, XBOOLE_0:def 4;
verum
end;
assume A5:
[x,y] in (R | X) /\ (R | Y)
; [x,y] in R | (X /\ Y)
then
[x,y] in R | Y
by XBOOLE_0:def 4;
then A6:
x in Y
by Def9;
A7:
[x,y] in R | X
by A5, XBOOLE_0:def 4;
then
x in X
by Def9;
then A8:
x in X /\ Y
by A6, XBOOLE_0:def 4;
[x,y] in R
by A7, Def9;
hence
[x,y] in R | (X /\ Y)
by A8, Def9; verum