let X be set ; :: thesis: for x being object
for R being reflexive total Relation of X st x in X holds
[x,x] in R
let x be object ; :: 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 ) ; :: thesis: verum