let Y be set ; :: thesis:
let R be Relation; :: thesis:
assume A1: ( Y c= field R & R is well-ordering ) ; :: thesis:
then A2: R |_2 Y is well-ordering by Th32;

now

given a being set such that A3: ( a in field (R |_2 Y) & R,(R |_2 Y) |_2 ((R |_2 Y) -Seg a) are_isomorphic ) ; :: thesis:
R |_2 Y is well-ordering by A1, Th32;
then A4: ( field (R |_2 Y) = Y & field ((R |_2 Y) |_2 ((R |_2 Y) -Seg a)) = (R |_2 Y) -Seg a ) by A1, Th39, Th40;
consider F being Function such that
A5: F is_isomorphism_of R,(R |_2 Y) |_2 ((R |_2 Y) -Seg a) by A3, Def8;
A6: ( dom F = field R & rng F = (R |_2 Y) -Seg a ) by A4, A5, Def7;
(R |_2 Y) -Seg a c= Y by A4, Th13;
then A7: rng F c= field R by A1, A6, XBOOLE_1:1;

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) & F . c <> F . b ) by A5, 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 A5, A8, Th45, XBOOLE_0:def 4; :: thesis:

end;

then A9: [a,(F . a)] in R by A1, A3, A4, A6, A7, Th43;
F . a in rng F by A1, A3, A4, A6, FUNCT_1:def 5;
then A10: ( [(F . a),a] in R |_2 Y & F . a <> a ) by A6, Def1;
then A11: [(F . a),a] in R by XBOOLE_0:def 4;
R is antisymmetric by A1, Def4;
hence contradiction by A9, A10, A11, Lm3; :: thesis:

end;

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 A1, A2, Th63; :: thesis: