let Y be set ; :: thesis: for R being Relation st Y c= field R & R is well-ordering & not R,R |_2 Y are_isomorphic holds
ex a being set st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic )
let R be Relation; :: thesis: ( Y c= field R & R is well-ordering & not R,R |_2 Y are_isomorphic implies ex a being set st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic ) )
assume that
A1: Y c= field R and
A2: R is well-ordering ; :: thesis: ( R,R |_2 Y are_isomorphic or ex a being set st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic ) )

A3: now :: thesis: for a being set holds
( not a in field (R |_2 Y) or not R,(R |_2 Y) |_2 ((R |_2 Y) -Seg a) are_isomorphic )

given a being set such that A4: a in field (R |_2 Y) and
A5: R,(R |_2 Y) |_2 ((R |_2 Y) -Seg a) are_isomorphic ; :: thesis: contradiction
consider F being Function such that
A6: F is_isomorphism_of R,(R |_2 Y) |_2 ((R |_2 Y) -Seg a) by A5, Def8;

A7: now :: thesis: for c, b being set st [c,b] in R & c <> b holds
( [(F . c),(F . b)] in R & F . c <> F . b )

let c, b be set ; :: thesis: ( [c,b] in R & c <> b implies ( [(F . c),(F . b)] in R & F . c <> F . b ) )
assume A8: ( [c,b] in R & c <> b ) ; :: thesis: ( [(F . c),(F . b)] in R & F . c <> F . b )
then [(F . c),(F . b)] in (R |_2 Y) |_2 ((R |_2 Y) -Seg a) by A6, Th36;
then [(F . c),(F . b)] in R |_2 Y by XBOOLE_0:def 4;
hence ( [(F . c),(F . b)] in R & F . c <> F . b ) by A6, A8, Th36, XBOOLE_0:def 4; :: thesis: verum

end;

A9: field (R |_2 Y) = Y by A1, A2, Th31;
field ((R |_2 Y) |_2 ((R |_2 Y) -Seg a)) = (R |_2 Y) -Seg a by A2, Th25, Th32;
then A10: rng F = (R |_2 Y) -Seg a by A6, Def7;
A11: dom F = field R by A6, Def7;
then A12: F . a in rng F by A1, A4, A9, FUNCT_1:def 3;
then A13: F . a <> a by A10, Th1;
[(F . a),a] in R |_2 Y by A10, A12, Th1;
then A14: [(F . a),a] in R by XBOOLE_0:def 4;
(R |_2 Y) -Seg a c= Y by A9, Th9;
then rng F c= field R by A1, A10, XBOOLE_1:1;
then [a,(F . a)] in R by A1, A2, A4, A9, A11, A7, Th35;
hence contradiction by A13, A14, A2, Lm3; :: thesis: verum

end;

R |_2 Y is well-ordering by A2, Th25;
hence ( R,R |_2 Y are_isomorphic or ex a being set st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic ) ) by A2, A3, Th52; :: thesis: verum