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 ~) )

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

hence
(R | X) ~ = X |` (R ~)
by RELAT_1:def 2; :: thesis: verum
let a, b be object ; :: thesis: ( [a,b] in (R | X) ~ iff [a,b] in X |` (R ~) )

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;hereby :: thesis: ( [a,b] in X |` (R ~) implies [a,b] in (R | X) ~ )

assume
[a,b] in X |` (R ~)
; :: thesis: [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;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

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