let R be Relation; :: thesis: for X being set holds (R | X) ~ = X |` (R ~)
let X be set ; :: thesis: (R | X) ~ = X |` (R ~)
for a, b being object holds
( [a,b] in (R | X) ~ iff [a,b] in X |` (R ~) )

proof

let a, b be object ; :: thesis: ( [a,b] in (R | X) ~ iff [a,b] in X |` (R ~) )

hereby :: thesis: ( [a,b] in X |` (R ~) implies [a,b] in (R | X) ~ )

assume [a,b] in (R | X) ~ ; :: thesis: [a,b] in X |` (R ~)
then [b,a] in R | X by RELAT_1:def 7;
then ( b in X & [b,a] in R ) by RELAT_1:def 11;
then ( b in X & [a,b] in R ~ ) by RELAT_1:def 7;
hence [a,b] in X |` (R ~) by RELAT_1:def 12; :: thesis: verum

end;

assume [a,b] in X |` (R ~) ; :: thesis: [a,b] in (R | X) ~
then ( b in X & [a,b] in R ~ ) by RELAT_1:def 12;
then ( b in X & [b,a] in R ) by RELAT_1:def 7;
then [b,a] in R | X by RELAT_1:def 11;
hence [a,b] in (R | X) ~ by RELAT_1:def 7; :: thesis: verum

end;

hence (R | X) ~ = X |` (R ~) by RELAT_1:def 2; :: thesis: verum