let R be Relation; for X being set holds (R |_2 X) ~ = (R ~) |_2 X
let X be set ; (R |_2 X) ~ = (R ~) |_2 X
now for x, y being object holds
( ( [x,y] in (R ~) |_2 X implies [y,x] in R |_2 X ) & ( [y,x] in R |_2 X implies [x,y] in (R ~) |_2 X ) )let x,
y be
object ;
( ( [x,y] in (R ~) |_2 X implies [y,x] in R |_2 X ) & ( [y,x] in R |_2 X implies [x,y] in (R ~) |_2 X ) )thus
(
[x,y] in (R ~) |_2 X implies
[y,x] in R |_2 X )
( [y,x] in R |_2 X implies [x,y] in (R ~) |_2 X )proof
assume A1:
[x,y] in (R ~) |_2 X
;
[y,x] in R |_2 X
then
[x,y] in [:X,X:]
by XBOOLE_0:def 4;
then A2:
[y,x] in [:X,X:]
by ZFMISC_1:88;
[x,y] in R ~
by A1, XBOOLE_0:def 4;
then
[y,x] in R
by RELAT_1:def 7;
hence
[y,x] in R |_2 X
by A2, XBOOLE_0:def 4;
verum
end; assume A3:
[y,x] in R |_2 X
;
[x,y] in (R ~) |_2 Xthen
[y,x] in [:X,X:]
by XBOOLE_0:def 4;
then A4:
[x,y] in [:X,X:]
by ZFMISC_1:88;
[y,x] in R
by A3, XBOOLE_0:def 4;
then
[x,y] in R ~
by RELAT_1:def 7;
hence
[x,y] in (R ~) |_2 X
by A4, XBOOLE_0:def 4;
verum end;
hence
(R |_2 X) ~ = (R ~) |_2 X
by RELAT_1:def 7; verum