theorem :: ORDERS_1:77

for R being Relation
for X, Y being set st R well_orders X & Y c= X holds
R well_orders Y by Lm18;