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 be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in R |_2 X or [x,b₁] in (X | R) | X ) & ( not [x,b₁] in (X | R) | X or [x,b₁] in R |_2 X ) )
let y be set ; :: 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 [x,y] in R |_2 X ; :: thesis: [x,y] in (X | R) | X
then A1: ( [x,y] in R & [x,y] in [:X,X:] ) by XBOOLE_0:def 4;
then A2: ( x in X & y in X ) by ZFMISC_1:106;
then [x,y] in X | R by A1, RELAT_1:def 12;
hence [x,y] in (X | R) | X by A2, RELAT_1:def 11; :: thesis: verum

end;

assume [x,y] in (X | R) | X ; :: thesis: [x,y] in R |_2 X
then A3: ( [x,y] in X | R & x in X ) by RELAT_1:def 11;
then A4: ( [x,y] in R & y in X ) by RELAT_1:def 12;
then [x,y] in [:X,X:] by A3, ZFMISC_1:106;
hence [x,y] in R |_2 X by A4, XBOOLE_0:def 4; :: thesis: verum