let X be non empty set ; :: thesis: for R being Relation of X holds R = (((R ~) `) ~) `
let R be Relation of X; :: thesis: R = (((R ~) `) ~) `
for x, y being object st [x,y] in R holds
[x,y] in (((R ~) `) ~) `

proof

let x, y be object ; :: thesis: ( [x,y] in R implies [x,y] in (((R ~) `) ~) ` )
assume X0: [x,y] in R ; :: thesis: [x,y] in (((R ~) `) ~) `
then x1: ( x in field R & y in field R ) by RELAT_1:15;
[y,x] in R ~ by X0, RELAT_1:def 7;
then not [y,x] in (R ~) ` by XBOOLE_0:def 5;
then not [x,y] in ((R ~) `) ~ by RELAT_1:def 7;
hence [x,y] in (((R ~) `) ~) ` by x1, Lemma12b; :: thesis: verum

end;

then n1: R c= (((R ~) `) ~) ` by RELAT_1:def 3;
for x, y being object st [x,y] in (((R ~) `) ~) ` holds
[x,y] in R

proof

let x, y be object ; :: thesis: ( [x,y] in (((R ~) `) ~) ` implies [x,y] in R )
assume X0: [x,y] in (((R ~) `) ~) ` ; :: thesis: [x,y] in R
then x1: ( x in field ((((R ~) `) ~) `) & y in field ((((R ~) `) ~) `) ) by RELAT_1:15;
not [x,y] in ((R ~) `) ~ by XBOOLE_0:def 5, X0;
then not [y,x] in (R ~) ` by RELAT_1:def 7;
then [y,x] in R ~ by Lemma12b, x1;
hence [x,y] in R by RELAT_1:def 7; :: thesis: verum

end;

then (((R ~) `) ~) ` c= R by RELAT_1:def 3;
hence R = (((R ~) `) ~) ` by n1, XBOOLE_0:def 10; :: thesis: verum