theorem Th27: :: WELLORD1:27

for a, b being object
for R being Relation st R is well-ordering & b in R -Seg a holds
(R |_2 (R -Seg a)) -Seg b = R -Seg b