for Y being set
for R being Relation st R is well-ordering holds
R |_2 Y is well-ordering by Th15, Th16, Th17, Th18, Th24;