let X be set ; :: thesis: for O being Order of X holds O is being_quasi-order
let O be Order of X; :: thesis: O is being_quasi-order
O is being_partial-order by Def4;
hence O is being_quasi-order by Th109; :: thesis: verum