theorem Th45: :: ORDERS_1:45

for R being Relation
for X being set st R partially_orders X holds
R |_2 X is Order of X