theorem :: ORDERS_1:46
for R being Relation
for X being set st R linearly_orders X holds
R |_2 X is Order of X by Th29, Th45;