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:97;
hence id X c= R by RELAT_2:17; :: thesis: verum