theorem Th32: :: WELLORD1:32

for a being object
for R being Relation st R is well-ordering holds
field (R |_2 (R -Seg a)) = R -Seg a