theorem :: ORDERS_1:35

for R being Relation
for X, Y being set st R partially_orders Y & X c= Y holds
R partially_orders X