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