theorem :: ORDERS_1:27

for R being Relation
for X being set st R is being_linear-order holds
R |_2 X is being_linear-order by WELLORD1:15, WELLORD1:16, WELLORD1:17;