let X be set ; :: thesis: for R being Relation st ( for x being set st x in X holds
[x,x] in R ) holds
id X c= R
let R be Relation; :: thesis: ( ( for x being set st x in X holds
[x,x] in R ) implies id X c= R )
assume A1: for x being set st x in X holds
[x,x] in R ; :: thesis: id X c= R
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b being set st [x,b] in id X holds
[x,b] in R
let y be set ; :: thesis: ( [x,y] in id X implies [x,y] in R )
assume [x,y] in id X ; :: thesis: [x,y] in R
then ( x in X & x = y ) by Def10;
hence [x,y] in R by A1; :: thesis: verum