theorem Th46: :: WELLORD1:46

for R being Relation st R is well-ordering holds
for a being object st a in field R holds
not R,R |_2 (R -Seg a) are_isomorphic