let R be Relation; :: thesis: for X being set st R is being_quasi-order holds
R |_2 X is being_quasi-order
let X be set ; :: thesis: ( R is being_quasi-order implies R |_2 X is being_quasi-order )
assume ( R is reflexive & R is transitive ) ; :: according to ORDERS_1:def 3 :: thesis: R |_2 X is being_quasi-order
hence ( R |_2 X is reflexive & R |_2 X is transitive ) by WELLORD1:22, WELLORD1:24; :: according to ORDERS_1:def 3 :: thesis: verum