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 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
A1: ( [x,y] in R & y in X /\ Y ) by Def14;
( y in X & y in Y & [x,y] in R ) by A1, XBOOLE_0:def 4;
then ( x in R " X & x in R " Y ) by Def14;
hence x in (R " X) /\ (R " Y) by XBOOLE_0:def 4; :: thesis: verum