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 )
proof
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;
assume A5: [x,y] in (X |` R) | X ; :: thesis: [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