let X be set ; :: thesis: for R being Relation st R c= [:X,X:] holds
( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) )
let R be Relation; :: thesis: ( R c= [:X,X:] implies ( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) ) )
A1: R \ (id (dom R)) c= R \ (id X)

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R \ (id (dom R)) or [x,y] in R \ (id X) )
assume A2: [x,y] in R \ (id (dom R)) ; :: thesis: [x,y] in R \ (id X)
then A3: not [x,y] in id (dom R) by XBOOLE_0:def 5;
not [x,y] in id X

proof

assume [x,y] in id X ; :: thesis: contradiction
then A4: x = y by RELAT_1:def 10;
x in dom R by A2, XTUPLE_0:def 12;
hence contradiction by A3, A4, RELAT_1:def 10; :: thesis: verum

end;

hence [x,y] in R \ (id X) by A2, XBOOLE_0:def 5; :: thesis: verum

end;

A5: R \ (id (rng R)) c= R \ (id X)

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R \ (id (rng R)) or [x,y] in R \ (id X) )
assume A6: [x,y] in R \ (id (rng R)) ; :: thesis: [x,y] in R \ (id X)
then A7: not [x,y] in id (rng R) by XBOOLE_0:def 5;
not [x,y] in id X

proof

assume [x,y] in id X ; :: thesis: contradiction
then A8: x = y by RELAT_1:def 10;
y in rng R by A6, XTUPLE_0:def 13;
hence contradiction by A7, A8, RELAT_1:def 10; :: thesis: verum

end;

hence [x,y] in R \ (id X) by A6, XBOOLE_0:def 5; :: thesis: verum

end;

assume A9: R c= [:X,X:] ; :: thesis: ( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) )
then id (dom R) c= id X by Th3, Th15;
then R \ (id X) c= R \ (id (dom R)) by XBOOLE_1:34;
hence R \ (id (dom R)) = R \ (id X) by A1; :: thesis: R \ (id (rng R)) = R \ (id X)
id (rng R) c= id X by A9, Th3, Th15;
then R \ (id X) c= R \ (id (rng R)) by XBOOLE_1:34;
hence R \ (id (rng R)) = R \ (id X) by A5; :: thesis: verum