theorem :: ORDERS_1:33

for R being Relation
for X being set st R quasi_orders X holds
R |_2 X is being_quasi-order by Lm8, Lm9;