let A, B be set ; :: thesis: for R being Relation of A,B holds R .: A = ((R ~) * R) .: B
let R be Relation of A,B; :: thesis: R .: A = ((R ~) * R) .: B
A1: ((R ~) * R) .: B = R .: ((R ~) .: B) by RELAT_1:126
.= R .: (proj1 R) by Th50 ;
thus R .: A c= ((R ~) * R) .: B :: according to XBOOLE_0:def 10 :: thesis: ((R ~) * R) .: B c= R .: A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R .: A or x in ((R ~) * R) .: B )
assume A2: x in R .: A ; :: thesis: x in ((R ~) * R) .: B
A3: R .: A = R .: (A /\ (proj1 R)) by Th46;
R .: (A /\ (proj1 R)) c= (R .: A) /\ (R .: (proj1 R)) by RELAT_1:121;
hence x in ((R ~) * R) .: B by A1, A2, A3, XBOOLE_0:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((R ~) * R) .: B or x in R .: A )
assume A4: x in ((R ~) * R) .: B ; :: thesis: x in R .: A
proj1 R c= dom R ;
then R .: (proj1 R) c= R .: A by RELAT_1:123;
hence x in R .: A by A1, A4; :: thesis: verum