for R being Relation
for X being set st R well_orders X holds
R |_2 X is Order of X by Th28, Th45;