let R be Relation; :: thesis: for X being set holds (R |_2 X) ~ = (R ~) |_2 X
let X be set ; :: thesis: (R |_2 X) ~ = (R ~) |_2 X
now :: thesis: 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 ; :: thesis: ( ( [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 ) :: thesis: ( [y,x] in R |_2 X implies [x,y] in (R ~) |_2 X )
proof
assume A1: [x,y] in (R ~) |_2 X ; :: thesis: [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; :: thesis: verum
end;
assume A3: [y,x] in R |_2 X ; :: thesis: [x,y] in (R ~) |_2 X
then [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; :: thesis: verum
end;
hence (R |_2 X) ~ = (R ~) |_2 X by RELAT_1:def 7; :: thesis: verum