let Y be set ; :: thesis:
let R be Relation; :: thesis:
assume that
A1: Y c= field R and
A2: R is well-ordering ; :: thesis:

A3: now :: thesis:

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

A7: now :: thesis:

let c, b be object ; :: thesis:
assume A8: ( [c,b] in R & c <> b ) ; :: thesis:
then [(F . c),(F . b)] in (R |_2 Y) |_2 ((R |_2 Y) -Seg a) by A6;
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:

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;
A11: dom F = field R by A6;
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;
then [a,(F . a)] in R by A1, A2, A4, A9, A11, A7, Th35;
hence contradiction by A13, A14, A2, Lm3; :: thesis:

end;

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