let R be Relation; :: thesis: ( R is well-ordering & ( for a being object st a in field R holds
ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic ) implies ex A being Ordinal st R, RelIncl A are_isomorphic )

assume A1: R is well-ordering ; :: thesis: ( ex a being object st
( a in field R & ( for A being Ordinal holds not R |_2 (R -Seg a), RelIncl A are_isomorphic ) ) or ex A being Ordinal st R, RelIncl A are_isomorphic )

defpred S1[ object , object ] means for A being Ordinal holds
( A = \$2 iff R |_2 (R -Seg \$1), RelIncl A are_isomorphic );
assume A2: for a being object st a in field R holds
ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic ; :: thesis: ex A being Ordinal st R, RelIncl A are_isomorphic
A3: for a being object st a in field R holds
ex b being object st S1[a,b]
proof
let a be object ; :: thesis: ( a in field R implies ex b being object st S1[a,b] )
assume a in field R ; :: thesis: ex b being object st S1[a,b]
then consider A being Ordinal such that
A4: R |_2 (R -Seg a), RelIncl A are_isomorphic by A2;
reconsider b = A as set ;
take b ; :: thesis: S1[a,b]
let B be Ordinal; :: thesis: ( B = b iff R |_2 (R -Seg a), RelIncl B are_isomorphic )
thus ( B = b implies R |_2 (R -Seg a), RelIncl B are_isomorphic ) by A4; :: thesis: ( R |_2 (R -Seg a), RelIncl B are_isomorphic implies B = b )
assume R |_2 (R -Seg a), RelIncl B are_isomorphic ; :: thesis: B = b
hence B = b by ; :: thesis: verum
end;
A5: for b, c, d being object st b in field R & S1[b,c] & S1[b,d] holds
c = d
proof
let b, c, d be object ; :: thesis: ( b in field R & S1[b,c] & S1[b,d] implies c = d )
assume that
A6: b in field R and
A7: for A being Ordinal holds
( A = c iff R |_2 (R -Seg b), RelIncl A are_isomorphic ) and
A8: for B being Ordinal holds
( B = d iff R |_2 (R -Seg b), RelIncl B are_isomorphic ) ; :: thesis: c = d
consider A being Ordinal such that
A9: R |_2 (R -Seg b), RelIncl A are_isomorphic by A2, A6;
A = c by A7, A9;
hence c = d by A8, A9; :: thesis: verum
end;
consider H being Function such that
A10: ( dom H = field R & ( for b being object st b in field R holds
S1[b,H . b] ) ) from for a being object st a in rng H holds
a is Ordinal
proof
let b be object ; :: thesis: ( b in rng H implies b is Ordinal )
assume b in rng H ; :: thesis: b is Ordinal
then consider c being object such that
A11: c in dom H and
A12: b = H . c by FUNCT_1:def 3;
ex A being Ordinal st R |_2 (R -Seg c), RelIncl A are_isomorphic by A2, A10, A11;
hence b is Ordinal by ; :: thesis: verum
end;
then consider C being Ordinal such that
A13: rng H c= C by ORDINAL1:24;
A14: now :: thesis: for b being object st b in rng H holds
for c being object st [c,b] in RelIncl C holds
c in rng H
let b be object ; :: thesis: ( b in rng H implies for c being object st [c,b] in RelIncl C holds
c in rng H )

assume A15: b in rng H ; :: thesis: for c being object st [c,b] in RelIncl C holds
c in rng H

then consider b9 being object such that
A16: b9 in dom H and
A17: b = H . b9 by FUNCT_1:def 3;
set V = R -Seg b9;
set P = R |_2 (R -Seg b9);
consider A being Ordinal such that
A18: R |_2 (R -Seg b9), RelIncl A are_isomorphic by A2, A10, A16;
let c be object ; :: thesis: ( [c,b] in RelIncl C implies c in rng H )
assume A19: [c,b] in RelIncl C ; :: thesis: c in rng H
A20: A = b by A10, A16, A17, A18;
now :: thesis: ( c <> b implies c in rng H )
A21: C = field () by Def1;
then A22: c in C by ;
then reconsider B = c as Ordinal ;
b in C by ;
then A23: B c= A by ;
then A24: (RelIncl A) |_2 B = RelIncl B by Th1;
assume c <> b ; :: thesis: c in rng H
then A25: B c< A by ;
then A26: B = () -Seg B by ;
A27: A = field () by Def1;
RelIncl A,R |_2 (R -Seg b9) are_isomorphic by ;
then canonical_isomorphism_of ((),(R |_2 (R -Seg b9))) is_isomorphism_of RelIncl A,R |_2 (R -Seg b9) by WELLORD1:def 9;
then consider d being object such that
A28: d in field (R |_2 (R -Seg b9)) and
A29: (RelIncl A) |_2 (() -Seg B),(R |_2 (R -Seg b9)) |_2 ((R |_2 (R -Seg b9)) -Seg d) are_isomorphic by ;
A30: d in field R by ;
A31: (R |_2 (R -Seg b9)) -Seg d = R -Seg d by ;
d in R -Seg b9 by ;
then [d,b9] in R by WELLORD1:1;
then R -Seg d c= R -Seg b9 by ;
then RelIncl B,R |_2 (R -Seg d) are_isomorphic by ;
then R |_2 (R -Seg d), RelIncl B are_isomorphic by WELLORD1:40;
then B = H . d by ;
hence c in rng H by ; :: thesis: verum
end;
hence c in rng H by A15; :: thesis: verum
end;
A32: ( ex a being object st
( a in C & rng H = () -Seg a ) implies rng H is Ordinal ) by Th3;
( C = field () & RelIncl C is well-ordering ) by Def1;
then reconsider A = rng H as Ordinal by ;
take A ; :: thesis:
take H ; :: according to WELLORD1:def 8 :: thesis:
thus dom H = field R by A10; :: according to WELLORD1:def 7 :: thesis: ( rng H = field () & H is one-to-one & ( for b1, b2 being object holds
( ( not [b1,b2] in R or ( b1 in field R & b2 in field R & [(H . b1),(H . b2)] in RelIncl A ) ) & ( not b1 in field R or not b2 in field R or not [(H . b1),(H . b2)] in RelIncl A or [b1,b2] in R ) ) ) )

thus rng H = field () by Def1; :: thesis: ( H is one-to-one & ( for b1, b2 being object holds
( ( not [b1,b2] in R or ( b1 in field R & b2 in field R & [(H . b1),(H . b2)] in RelIncl A ) ) & ( not b1 in field R or not b2 in field R or not [(H . b1),(H . b2)] in RelIncl A or [b1,b2] in R ) ) ) )

A33: for a being object st a in dom H holds
H . a is Ordinal
proof
let a be object ; :: thesis: ( a in dom H implies H . a is Ordinal )
assume a in dom H ; :: thesis: H . a is Ordinal
then H . a in A by FUNCT_1:def 3;
hence H . a is Ordinal ; :: thesis: verum
end;
thus A34: H is one-to-one :: thesis: for b1, b2 being object holds
( ( not [b1,b2] in R or ( b1 in field R & b2 in field R & [(H . b1),(H . b2)] in RelIncl A ) ) & ( not b1 in field R or not b2 in field R or not [(H . b1),(H . b2)] in RelIncl A or [b1,b2] in R ) )
proof
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom H or not b in dom H or not H . a = H . b or a = b )
assume that
A35: a in dom H and
A36: b in dom H and
A37: H . a = H . b ; :: thesis: a = b
reconsider B = H . a as Ordinal by ;
R |_2 (R -Seg b), RelIncl B are_isomorphic by ;
then A38: RelIncl B,R |_2 (R -Seg b) are_isomorphic by WELLORD1:40;
R |_2 (R -Seg a), RelIncl B are_isomorphic by ;
then R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by ;
hence a = b by ; :: thesis: verum
end;
let a, b be object ; :: thesis: ( ( not [a,b] in R or ( a in field R & b in field R & [(H . a),(H . b)] in RelIncl A ) ) & ( not a in field R or not b in field R or not [(H . a),(H . b)] in RelIncl A or [a,b] in R ) )
thus ( [a,b] in R implies ( a in field R & b in field R & [(H . a),(H . b)] in RelIncl A ) ) :: thesis: ( not a in field R or not b in field R or not [(H . a),(H . b)] in RelIncl A or [a,b] in R )
proof
set Z = R -Seg b;
set P = R |_2 (R -Seg b);
A39: ( A = field () & R |_2 (R -Seg b) is well-ordering ) by ;
assume A40: [a,b] in R ; :: thesis: ( a in field R & b in field R & [(H . a),(H . b)] in RelIncl A )
hence A41: ( a in field R & b in field R ) by RELAT_1:15; :: thesis: [(H . a),(H . b)] in RelIncl A
then reconsider A9 = H . a, B9 = H . b as Ordinal by ;
A42: R |_2 (R -Seg b), RelIncl B9 are_isomorphic by ;
A43: A9 in A by ;
A44: B9 in A by ;
A45: R |_2 (R -Seg a), RelIncl A9 are_isomorphic by ;
now :: thesis: ( a <> b implies [A9,B9] in RelIncl A )
assume a <> b ; :: thesis: [A9,B9] in RelIncl A
then A46: a in R -Seg b by ;
then A47: (R |_2 (R -Seg b)) -Seg a = R -Seg a by ;
R -Seg b c= field R by WELLORD1:9;
then A48: a in field (R |_2 (R -Seg b)) by ;
A9 c= A by ;
then A49: (RelIncl A) |_2 A9 = RelIncl A9 by Th1;
( A9 = () -Seg A9 & R -Seg a c= R -Seg b ) by ;
then A50: (R |_2 (R -Seg b)) |_2 ((R |_2 (R -Seg b)) -Seg a),() |_2 (() -Seg A9) are_isomorphic by ;
( B9 = () -Seg B9 & B9 c= A ) by ;
then R |_2 (R -Seg b),() |_2 (() -Seg B9) are_isomorphic by ;
hence [A9,B9] in RelIncl A by ; :: thesis: verum
end;
hence [(H . a),(H . b)] in RelIncl A by ; :: thesis: verum
end;
assume that
A51: a in field R and
A52: b in field R and
A53: [(H . a),(H . b)] in RelIncl A ; :: thesis: [a,b] in R
assume A54: not [a,b] in R ; :: thesis: contradiction
R is_reflexive_in field R by ;
then A55: a <> b by ;
R is_connected_in field R by ;
then A56: [b,a] in R by A51, A52, A54, A55;
then A57: R -Seg b c= R -Seg a by ;
A58: RelIncl A is_antisymmetric_in field () by RELAT_2:def 12;
A59: A = field () by Def1;
reconsider A9 = H . a, B9 = H . b as Ordinal by A10, A33, A51, A52;
A60: R |_2 (R -Seg a), RelIncl A9 are_isomorphic by ;
A61: R |_2 (R -Seg b), RelIncl B9 are_isomorphic by ;
A62: B9 in A by ;
then B9 c= A by ORDINAL1:def 2;
then A63: (RelIncl A) |_2 B9 = RelIncl B9 by Th1;
set Z = R -Seg a;
set P = R |_2 (R -Seg a);
A64: A9 in A by ;
then ( A9 = () -Seg A9 & A9 c= A ) by ;
then A65: R |_2 (R -Seg a),() |_2 (() -Seg A9) are_isomorphic by ;
A66: b in R -Seg a by ;
then A67: (R |_2 (R -Seg a)) -Seg b = R -Seg b by ;
B9 = () -Seg B9 by ;
then A68: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),() |_2 (() -Seg B9) are_isomorphic by ;
R -Seg a c= field R by WELLORD1:9;
then A69: b in field (R |_2 (R -Seg a)) by ;
R |_2 (R -Seg a) is well-ordering by ;
then [B9,A9] in RelIncl A by ;
then H . a = H . b by A53, A58, A64, A62, A59;
hence contradiction by A10, A34, A51, A52, A55; :: thesis: verum