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 Lm4;
then O is_reflexive_in X by RELAT_2:def 9;
hence ( x in X implies [x,x] in O ) ; :: thesis: verum