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

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