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 object 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 object 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 object st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic ) )

A3: now :: thesis: for a being object 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 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: contradiction
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: for c, b being object st [c,b] in R & c <> b holds
( [(F . c),(F . b)] in R & F . c <> F . b )
let c, b be object ; :: 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;
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 ; :: 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 ;
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 ;
then A13: F . a <> a by ;
[(F . a),a] in R |_2 Y by ;
then A14: [(F . a),a] in R by XBOOLE_0:def 4;
(R |_2 Y) -Seg a c= Y by ;
then rng F c= field R by ;
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 ;
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: verum