let X, x, y be set ; :: thesis: for O being Order of X st x in X & y in X & [x,y] in O & [y,x] in O holds
x = y
let O be Order of X; :: thesis: ( x in X & y in X & [x,y] in O & [y,x] in O implies x = y )
field O = X by Lm2;
then O is_antisymmetric_in X by RELAT_2:def 12;
hence ( x in X & y in X & [x,y] in O & [y,x] in O implies x = y ) by RELAT_2:def 4; :: thesis: verum