let x be object ; :: thesis: ( x in (X |` P) * R implies x in P * (R | X) )
assume A2: x in (X |` P) * R ; :: thesis: x in P * (R | X)
then consider y, z being object such that
A3: x = [y,z] by RELAT_1:def 1;
consider w being object such that
A4: [y,w] in X |` P and
A5: [w,z] in R by A2, A3, RELAT_1:def 8;
w in X by A4, RELAT_1:def 12;
then A6: [w,z] in R | X by A5, RELAT_1:def 11;
[y,w] in P by A4, RELAT_1:def 12;
hence x in P * (R | X) by A3, A6, RELAT_1:def 8; :: thesis: verum

let x be object ; :: thesis: ( x in P * (R | X) implies x in (X |` P) * R )
assume A7: x in P * (R | X) ; :: thesis: x in (X |` P) * R
then consider y, z being object such that
A8: x = [y,z] by RELAT_1:def 1;
consider w being object such that
A9: [y,w] in P and
A10: [w,z] in R | X by A7, A8, RELAT_1:def 8;
w in X by A10, RELAT_1:def 11;
then A11: [y,w] in X |` P by A9, RELAT_1:def 12;
[w,z] in R by A10, RELAT_1:def 11;
hence x in (X |` P) * R by A8, A11, RELAT_1:def 8; :: thesis: verum