theorem Th50: :: WELLORD1:50

for R, S being Relation
for F being Function st R is well-ordering & F is_isomorphism_of R,S holds
for a being object st a in field R holds
ex b being object st
( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )