theorem Th31: :: WELLORD1:31

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