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 object ; :: 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 object such that
A1: [x,y] in R and
A2: x in X /\ Y by Def11;
x in Y by A2, XBOOLE_0:def 4;
then A3: y in R .: Y by A1, Def11;
x in X by A2, XBOOLE_0:def 4;
then y in R .: X by A1, Def11;
hence y in (R .: X) /\ (R .: Y) by A3, XBOOLE_0:def 4; :: thesis: verum