let X, Y be set ; :: thesis: for R being Relation holds (R | X) " Y = X /\ (R " Y)
let R be Relation; :: thesis: (R | X) " Y = X /\ (R " Y)
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: X /\ (R " Y) c= (R | X) " Y
let x be object ; :: thesis: ( x in (R | X) " Y implies x in X /\ (R " Y) )
assume x in (R | X) " Y ; :: thesis: x in X /\ (R " Y)
then A1: ex y being object st
( [x,y] in R | X & y in Y ) by RELAT_1:def 14;
then A2: x in X by RELAT_1:def 11;
R | X c= R by RELAT_1:59;
then x in R " Y by A1, RELAT_1:def 14;
hence x in X /\ (R " Y) by A2, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X /\ (R " Y) or x in (R | X) " Y )
assume A3: x in X /\ (R " Y) ; :: thesis: x in (R | X) " Y
then x in R " Y by XBOOLE_0:def 4;
then consider y being object such that
A4: [x,y] in R and
A5: y in Y by RELAT_1:def 14;
x in X by A3, XBOOLE_0:def 4;
then [x,y] in R | X by A4, RELAT_1:def 11;
hence x in (R | X) " Y by A5, RELAT_1:def 14; :: thesis: verum