let X be set ; :: thesis: for x being object
for T being reflexive total Relation of X holds
( x in X iff [x,x] in T )
let x be object ; :: 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 )
thus ( x in X implies [x,x] in T ) by EQREL_1:5; :: thesis: ( [x,x] in T implies x in X )
assume A1: [x,x] in T ; :: thesis: x in X
field T = X by ORDERS_1:12;
hence x in X by A1, RELAT_1:15; :: thesis: verum