let X be non empty set ; for R being Relation of X holds R = (((R ~) `) ~) `
let R be Relation of X; R = (((R ~) `) ~) `
for x, y being object st [x,y] in R holds
[x,y] in (((R ~) `) ~) `
proof
let x,
y be
object ;
( [x,y] in R implies [x,y] in (((R ~) `) ~) ` )
assume X0:
[x,y] in R
;
[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;
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 ;
( [x,y] in (((R ~) `) ~) ` implies [x,y] in R )
assume X0:
[x,y] in (((R ~) `) ~) `
;
[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;
verum
end;
then
(((R ~) `) ~) ` c= R
by RELAT_1:def 3;
hence
R = (((R ~) `) ~) `
by n1, XBOOLE_0:def 10; verum