theorem :: ROUGHS_1:3

for X being set
for R being Relation of X holds
( ( R is total & R is reflexive ) iff id X c= R )