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