let X be set ; for R being Relation holds R |_2 X = (X |` R) | X
let R be Relation; R |_2 X = (X |` R) | X
let x, y be object ; RELAT_1:def 2 ( ( 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 )
( not [x,y] in (X |` R) | X or [x,y] in R |_2 X )proof
assume A1:
[x,y] in R |_2 X
;
[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;
verum
end;
assume A5:
[x,y] in (X |` R) | X
; [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; verum