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

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:
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

let c, b be set ; :: 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, Th45;
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, Th45, XBOOLE_0:def 4; :: thesis:

end;

A9: R is antisymmetric by A2, Def4;
A10: field (R |_2 Y) = Y by A1, A2, Th39;
field ((R |_2 Y) |_2 ((R |_2 Y) -Seg a)) = (R |_2 Y) -Seg a by A2, Th32, Th40;
then A11: rng F = (R |_2 Y) -Seg a by A6, Def7;
A12: dom F = field R by A6, Def7;
then A13: F . a in rng F by A1, A4, A10, FUNCT_1:def 3;
then A14: F . a <> a by A11, Th1;
[(F . a),a] in R |_2 Y by A11, A13, Th1;
then A15: [(F . a),a] in R by XBOOLE_0:def 4;
(R |_2 Y) -Seg a c= Y by A10, Th13;
then rng F c= field R by A1, A11, XBOOLE_1:1;
then [a,(F . a)] in R by A1, A2, A4, A10, A12, A7, Th43;
hence contradiction by A14, A15, A9, Lm3; :: thesis:

end;

R |_2 Y is well-ordering by A2, Th32;
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, Th63; :: thesis: