theorem :: ROUGHS_1:3

for X being set
for R being reflexive total Relation of X holds id X c= R