let X be set ; :: thesis: for R1, R2 being Relation holds (R1 /\ R2) .: {_{X}_} c= (R1 .: {_{X}_}) /\ (R2 .: {_{X}_})
let R1, R2 be Relation; :: thesis: (R1 /\ R2) .: {_{X}_} c= (R1 .: {_{X}_}) /\ (R2 .: {_{X}_})
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (R1 /\ R2) .: {_{X}_} or y in (R1 .: {_{X}_}) /\ (R2 .: {_{X}_}) )
assume y in (R1 /\ R2) .: {_{X}_} ; :: thesis: y in (R1 .: {_{X}_}) /\ (R2 .: {_{X}_})
then consider x being object such that
A1: [x,y] in R1 /\ R2 and
A2: x in {_{X}_} by RELAT_1:def 13;
A3: [x,y] in R1 by A1, XBOOLE_0:def 4;
A4: [x,y] in R2 by A1, XBOOLE_0:def 4;
A5: y in R1 .: {_{X}_} by A2, A3, RELAT_1:def 13;
y in R2 .: {_{X}_} by A2, A4, RELAT_1:def 13;
hence y in (R1 .: {_{X}_}) /\ (R2 .: {_{X}_}) by A5, XBOOLE_0:def 4; :: thesis: verum