let R be Relation; :: thesis: for X being set st R quasi_orders X holds
R |_2 X is being_quasi-order
let X be set ; :: thesis: ( R quasi_orders X implies R |_2 X is being_quasi-order )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X ; :: according to ORDERS_1:def 6 :: thesis: R |_2 X is being_quasi-order
thus ( R |_2 X is reflexive & R |_2 X is transitive ) by A1, A2, Lm6, Lm7; :: according to ORDERS_1:def 3 :: thesis: verum