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