let X be set ; :: thesis: for O being Order of X holds O quasi_orders X
let O be Order of X; :: thesis: O quasi_orders X
field O = X by Lm2;
then ( O is_reflexive_in X & O is_transitive_in X ) by RELAT_2:def 9, RELAT_2:def 16;
hence O quasi_orders X by Def6; :: thesis: verum