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

end;

let y be object ; :: 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 object such that
A3: [x,y] in R ~ and
A4: x in Y /\ (proj2 R) by RELAT_1:def 13;
x in Y by A4, XBOOLE_0:def 4;
hence y in (R ~) .: Y by A3, RELAT_1:def 13; :: thesis: verum