theorem :: ORDERS_1:32

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