let X, Y be set ; :: thesis: for R being Relation holds R " (X /\ Y) c= (R " X) /\ (R " Y)
let R be Relation; :: thesis: R " (X /\ Y) c= (R " X) /\ (R " Y)
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 Y by A2, XBOOLE_0:def 4;
then A3: x in R " Y by A1, Def12;
y in X by A2, XBOOLE_0:def 4;
then x in R " X by A1, Def12;
hence x in (R " X) /\ (R " Y) by A3, XBOOLE_0:def 4; :: thesis: verum