theorem :: WELLORD1:53

for Y being set
for R being Relation st Y c= field R & R is well-ordering & not R,R |_2 Y are_isomorphic holds
ex a being object st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic )