theorem Th33: :: WELLORD1:33
for R being Relation st R is well-ordering holds
for Z being set st ( for a being object st a in field R & R -Seg a c= Z holds
a in Z ) holds
field R c= Z