let X be set ; :: thesis: for R being total reflexive Relation of X holds id X c= R
let R be total reflexive Relation of X; :: thesis: id X c= R
field R = X by ORDERS_1:97;
hence id X c= R by RELAT_2:17; :: thesis: verum