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