let A, B 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:126
.= (R ~) .: (proj2 R) by Th50 ;
thus (R ~) .: B c= (R * (R ~)) .: A :: according to XBOOLE_0:def 10 :: thesis: (R * (R ~)) .: A c= (R ~) .: B

proof

let x be object ; :: 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 Th47;
(R ~) .: (B /\ (proj2 R)) c= ((R ~) .: B) /\ ((R ~) .: (proj2 R)) by RELAT_1:121;
hence x in (R * (R ~)) .: A 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 ~)) .: A or x in (R ~) .: B )
assume A4: x in (R * (R ~)) .: A ; :: thesis: x in (R ~) .: B
proj2 R c= rng R ;
then (R ~) .: (proj2 R) c= (R ~) .: B by RELAT_1:123;
hence x in (R ~) .: B by A1, A4; :: thesis: verum