theorem :: ORDERS_1:39

for R being Relation
for X being set st R linearly_orders X holds
R |_2 X is being_linear-order by Lm8, Lm9, Lm10, Lm11;