let X, x be set ; :: thesis: for O being Order of X st x in X holds
[x,x] in O
let O be Order of X; :: thesis: ( x in X implies [x,x] in O )
field O = X by Lm2;
then O is_reflexive_in X by RELAT_2:def 9;
hence ( x in X implies [x,x] in O ) by RELAT_2:def 1; :: thesis: verum