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

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

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 )

R |_2 Y is well-ordering
by A2, Th25;( 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;

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

end;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 )

A9:
field (R |_2 Y) = Y
by A1, A2, Th31;( [(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 A6, A8, Th36, XBOOLE_0:def 4; :: thesis: verum

end;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 A6, A8, Th36, XBOOLE_0:def 4; :: thesis: verum

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

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