theorem :: RELAT_1:47

for X being set
for R being Relation st ( for x being object st x in X holds
[x,x] in R ) holds
id X c= R