let X, x be set ; :: thesis: for R being reflexive total Relation of X st x in X holds
[x,x] in R
let R be reflexive total Relation of X; :: thesis: ( x in X implies [x,x] in R )
field R = X by ORDERS_1:12;
then R is_reflexive_in X by RELAT_2:def 9;
hence ( x in X implies [x,x] in R ) by RELAT_2:def 1; :: thesis: verum