let A, B be set ; :: thesis: for R being Subset of [:A,B:]
for Y being set holds (R ~ ) .: Y = (R ~ ) .: (Y /\ (proj2 R))
let R be Subset of [:A,B:]; :: thesis: for Y being set holds (R ~ ) .: Y = (R ~ ) .: (Y /\ (proj2 R))
let Y be set ; :: thesis: (R ~ ) .: Y = (R ~ ) .: (Y /\ (proj2 R))
thus (R ~ ) .: Y c= (R ~ ) .: (Y /\ (proj2 R)) :: according to XBOOLE_0:def 10 :: thesis: (R ~ ) .: (Y /\ (proj2 R)) c= (R ~ ) .: Y

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (R ~ ) .: Y or y in (R ~ ) .: (Y /\ (proj2 R)) )
assume y in (R ~ ) .: Y ; :: thesis: y in (R ~ ) .: (Y /\ (proj2 R))
then consider x being set such that
A1: ( [x,y] in R ~ & x in Y ) by RELAT_1:def 13;
[y,x] in R by A1, RELAT_1:def 7;
then x in proj2 R by RELAT_1:def 5;
then x in Y /\ (proj2 R) by A1, XBOOLE_0:def 4;
hence y in (R ~ ) .: (Y /\ (proj2 R)) by A1, RELAT_1:def 13; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (R ~ ) .: (Y /\ (proj2 R)) or y in (R ~ ) .: Y )
assume y in (R ~ ) .: (Y /\ (proj2 R)) ; :: thesis: y in (R ~ ) .: Y
then consider x being set such that
A2: ( [x,y] in R ~ & x in Y /\ (proj2 R) ) by RELAT_1:def 13;
x in Y by A2, XBOOLE_0:def 4;
hence y in (R ~ ) .: Y by A2, RELAT_1:def 13; :: thesis: verum