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
A1: field O = X by Lm4;
then A2: O is_transitive_in X by RELAT_2:def 16;
O is_reflexive_in X by A1, RELAT_2:def 9;
hence O quasi_orders X by A2; :: thesis: verum