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