let X be set ; :: thesis: for R being Relation holds R |_2 X = (X |` R) | X

let R be Relation; :: thesis: R |_2 X = (X |` R) | X

let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in R |_2 X or [x,y] in (X |` R) | X ) & ( not [x,y] in (X |` R) | X or [x,y] in R |_2 X ) )

thus ( [x,y] in R |_2 X implies [x,y] in (X |` R) | X ) :: thesis: ( not [x,y] in (X |` R) | X or [x,y] in R |_2 X )

then A6: [x,y] in X |` R by RELAT_1:def 11;

then A7: [x,y] in R by RELAT_1:def 12;

A8: y in X by A6, RELAT_1:def 12;

x in X by A5, RELAT_1:def 11;

then [x,y] in [:X,X:] by A8, ZFMISC_1:87;

hence [x,y] in R |_2 X by A7, XBOOLE_0:def 4; :: thesis: verum

let R be Relation; :: thesis: R |_2 X = (X |` R) | X

let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in R |_2 X or [x,y] in (X |` R) | X ) & ( not [x,y] in (X |` R) | X or [x,y] in R |_2 X ) )

thus ( [x,y] in R |_2 X implies [x,y] in (X |` R) | X ) :: thesis: ( not [x,y] in (X |` R) | X or [x,y] in R |_2 X )

proof

assume A5:
[x,y] in (X |` R) | X
; :: thesis: [x,y] in R |_2 X
assume A1:
[x,y] in R |_2 X
; :: thesis: [x,y] in (X |` R) | X

then A2: [x,y] in [:X,X:] by XBOOLE_0:def 4;

then A3: x in X by ZFMISC_1:87;

A4: y in X by A2, ZFMISC_1:87;

[x,y] in R by A1, XBOOLE_0:def 4;

then [x,y] in X |` R by A4, RELAT_1:def 12;

hence [x,y] in (X |` R) | X by A3, RELAT_1:def 11; :: thesis: verum

end;then A2: [x,y] in [:X,X:] by XBOOLE_0:def 4;

then A3: x in X by ZFMISC_1:87;

A4: y in X by A2, ZFMISC_1:87;

[x,y] in R by A1, XBOOLE_0:def 4;

then [x,y] in X |` R by A4, RELAT_1:def 12;

hence [x,y] in (X |` R) | X by A3, RELAT_1:def 11; :: thesis: verum

then A6: [x,y] in X |` R by RELAT_1:def 11;

then A7: [x,y] in R by RELAT_1:def 12;

A8: y in X by A6, RELAT_1:def 12;

x in X by A5, RELAT_1:def 11;

then [x,y] in [:X,X:] by A8, ZFMISC_1:87;

hence [x,y] in R |_2 X by A7, XBOOLE_0:def 4; :: thesis: verum