let X, x be set ; :: thesis: for T being reflexive total Relation of X holds
( x in X iff [x,x] in T )
let T be reflexive total Relation of X; :: thesis: ( x in X iff [x,x] in T )
A1: field T = X by ORDERS_1:97;
thus ( x in X implies [x,x] in T ) by EQREL_1:11; :: thesis: ( [x,x] in T implies x in X )
assume [x,x] in T ; :: thesis: x in X
hence x in X by A1, RELAT_1:30; :: thesis: verum