for R being Relation
for X being set st R partially_orders X holds
R |_2 X is being_partial-order by Lm8, Lm9, Lm10;