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

proof

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

end;

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