theorem Th10: :: WELLORD2:16

for X being set
for R being Relation st R well_orders X holds
( field (R |_2 X) = X & R |_2 X is well-ordering )