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 y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in R .: (X /\ Y) or y in (R .: X) /\ (R .: Y) )
assume y in R .: (X /\ Y) ; :: thesis: y in (R .: X) /\ (R .: Y)
then consider x being set such that
A1: ( [x,y] in R & x in X /\ Y ) by Def13;
( x in X & x in Y & [x,y] in R ) by A1, XBOOLE_0:def 4;
then ( y in R .: X & y in R .: Y ) by Def13;
hence y in (R .: X) /\ (R .: Y) by XBOOLE_0:def 4; :: thesis: verum