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 S_{1}[ 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 S_{1}[a,b]
_{1}[b,c] & S_{1}[b,d] holds

c = d

A10: ( dom H = field R & ( for b being object st b in field R holds

S_{1}[b,H . b] ) )
from FUNCT_1:sch 2(A5, A3);

for a being object st a in rng H holds

a is Ordinal

A13: rng H c= C by ORDINAL1:24;

( a in C & rng H = (RelIncl C) -Seg a ) implies rng H is Ordinal ) by Th3;

( C = field (RelIncl C) & RelIncl C is well-ordering ) by Def1;

then reconsider A = rng H as Ordinal by A13, A14, A32, WELLORD1:28;

take A ; :: thesis: R, RelIncl A are_isomorphic

take H ; :: according to WELLORD1:def 8 :: thesis: H is_isomorphism_of R, RelIncl A

thus dom H = field R by A10; :: according to WELLORD1:def 7 :: thesis: ( rng H = field (RelIncl A) & H is one-to-one & ( for b_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in R or ( b_{1} in field R & b_{2} in field R & [(H . b_{1}),(H . b_{2})] in RelIncl A ) ) & ( not b_{1} in field R or not b_{2} in field R or not [(H . b_{1}),(H . b_{2})] in RelIncl A or [b_{1},b_{2}] in R ) ) ) )

thus rng H = field (RelIncl A) by Def1; :: thesis: ( H is one-to-one & ( for b_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in R or ( b_{1} in field R & b_{2} in field R & [(H . b_{1}),(H . b_{2})] in RelIncl A ) ) & ( not b_{1} in field R or not b_{2} in field R or not [(H . b_{1}),(H . b_{2})] in RelIncl A or [b_{1},b_{2}] in R ) ) ) )

A33: for a being object st a in dom H holds

H . a is Ordinal_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in R or ( b_{1} in field R & b_{2} in field R & [(H . b_{1}),(H . b_{2})] in RelIncl A ) ) & ( not b_{1} in field R or not b_{2} in field R or not [(H . b_{1}),(H . b_{2})] in RelIncl A or [b_{1},b_{2}] 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 )

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 A1, RELAT_2:def 9;

then A55: a <> b by A51, A54;

R is_connected_in field R by A1, RELAT_2:def 14;

then A56: [b,a] in R by A51, A52, A54, A55;

then A57: R -Seg b c= R -Seg a by A1, A51, A52, WELLORD1:29;

A58: RelIncl A is_antisymmetric_in field (RelIncl A) by RELAT_2:def 12;

A59: A = field (RelIncl A) 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 A10, A51;

A61: R |_2 (R -Seg b), RelIncl B9 are_isomorphic by A10, A52;

A62: B9 in A by A10, A52, FUNCT_1:def 3;

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 A10, A51, FUNCT_1:def 3;

then ( A9 = (RelIncl A) -Seg A9 & A9 c= A ) by Th3, ORDINAL1:def 2;

then A65: R |_2 (R -Seg a),(RelIncl A) |_2 ((RelIncl A) -Seg A9) are_isomorphic by A60, Th1;

A66: b in R -Seg a by A54, A56, WELLORD1:1;

then A67: (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, WELLORD1:27;

B9 = (RelIncl A) -Seg B9 by A62, Th3;

then A68: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),(RelIncl A) |_2 ((RelIncl A) -Seg B9) are_isomorphic by A61, A63, A67, A57, WELLORD1:22;

R -Seg a c= field R by WELLORD1:9;

then A69: b in field (R |_2 (R -Seg a)) by A1, A66, WELLORD1:31;

R |_2 (R -Seg a) is well-ordering by A1, WELLORD1:25;

then [B9,A9] in RelIncl A by A69, A64, A62, A59, A65, A68, WELLORD1:51;

then H . a = H . b by A53, A58, A64, A62, A59;

hence contradiction by A10, A34, A51, A52, A55; :: thesis: verum

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 S

( 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 S

proof

A5:
for b, c, d being object st b in field R & S
let a be object ; :: thesis: ( a in field R implies ex b being object st S_{1}[a,b] )

assume a in field R ; :: thesis: ex b being object st S_{1}[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: S_{1}[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 A4, Th5; :: thesis: verum

end;assume a in field R ; :: thesis: ex b being object st S

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

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 A4, Th5; :: thesis: verum

c = d

proof

consider H being Function such that
let b, c, d be object ; :: thesis: ( b in field R & S_{1}[b,c] & S_{1}[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;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

A10: ( dom H = field R & ( for b being object st b in field R holds

S

for a being object st a in rng H holds

a is Ordinal

proof

then consider C being Ordinal such that
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 A10, A11, A12; :: thesis: verum

end;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 A10, A11, A12; :: thesis: verum

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

A32:
( ex a being object st 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;

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

hence
c in rng H
by A15; :: thesis: verumA21:
C = field (RelIncl C)
by Def1;

then A22: c in C by A19, RELAT_1:15;

then reconsider B = c as Ordinal ;

b in C by A19, A21, RELAT_1:15;

then A23: B c= A by A20, A19, A22, Def1;

then A24: (RelIncl A) |_2 B = RelIncl B by Th1;

assume c <> b ; :: thesis: c in rng H

then A25: B c< A by A20, A23;

then A26: B = (RelIncl A) -Seg B by Th3, ORDINAL1:11;

A27: A = field (RelIncl A) by Def1;

RelIncl A,R |_2 (R -Seg b9) are_isomorphic by A18, WELLORD1:40;

then canonical_isomorphism_of ((RelIncl A),(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 ((RelIncl A) -Seg B),(R |_2 (R -Seg b9)) |_2 ((R |_2 (R -Seg b9)) -Seg d) are_isomorphic by A25, A27, ORDINAL1:11, WELLORD1:50;

A30: d in field R by A28, WELLORD1:12;

A31: (R |_2 (R -Seg b9)) -Seg d = R -Seg d by A1, A28, WELLORD1:12, WELLORD1:27;

d in R -Seg b9 by A28, WELLORD1:12;

then [d,b9] in R by WELLORD1:1;

then R -Seg d c= R -Seg b9 by A1, A10, A16, A30, WELLORD1:29;

then RelIncl B,R |_2 (R -Seg d) are_isomorphic by A29, A26, A24, A31, WELLORD1:22;

then R |_2 (R -Seg d), RelIncl B are_isomorphic by WELLORD1:40;

then B = H . d by A10, A30;

hence c in rng H by A10, A30, FUNCT_1:def 3; :: thesis: verum

end;then A22: c in C by A19, RELAT_1:15;

then reconsider B = c as Ordinal ;

b in C by A19, A21, RELAT_1:15;

then A23: B c= A by A20, A19, A22, Def1;

then A24: (RelIncl A) |_2 B = RelIncl B by Th1;

assume c <> b ; :: thesis: c in rng H

then A25: B c< A by A20, A23;

then A26: B = (RelIncl A) -Seg B by Th3, ORDINAL1:11;

A27: A = field (RelIncl A) by Def1;

RelIncl A,R |_2 (R -Seg b9) are_isomorphic by A18, WELLORD1:40;

then canonical_isomorphism_of ((RelIncl A),(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 ((RelIncl A) -Seg B),(R |_2 (R -Seg b9)) |_2 ((R |_2 (R -Seg b9)) -Seg d) are_isomorphic by A25, A27, ORDINAL1:11, WELLORD1:50;

A30: d in field R by A28, WELLORD1:12;

A31: (R |_2 (R -Seg b9)) -Seg d = R -Seg d by A1, A28, WELLORD1:12, WELLORD1:27;

d in R -Seg b9 by A28, WELLORD1:12;

then [d,b9] in R by WELLORD1:1;

then R -Seg d c= R -Seg b9 by A1, A10, A16, A30, WELLORD1:29;

then RelIncl B,R |_2 (R -Seg d) are_isomorphic by A29, A26, A24, A31, WELLORD1:22;

then R |_2 (R -Seg d), RelIncl B are_isomorphic by WELLORD1:40;

then B = H . d by A10, A30;

hence c in rng H by A10, A30, FUNCT_1:def 3; :: thesis: verum

( a in C & rng H = (RelIncl C) -Seg a ) implies rng H is Ordinal ) by Th3;

( C = field (RelIncl C) & RelIncl C is well-ordering ) by Def1;

then reconsider A = rng H as Ordinal by A13, A14, A32, WELLORD1:28;

take A ; :: thesis: R, RelIncl A are_isomorphic

take H ; :: according to WELLORD1:def 8 :: thesis: H is_isomorphism_of R, RelIncl A

thus dom H = field R by A10; :: according to WELLORD1:def 7 :: thesis: ( rng H = field (RelIncl A) & H is one-to-one & ( for b

( ( not [b

thus rng H = field (RelIncl A) by Def1; :: thesis: ( H is one-to-one & ( for b

( ( not [b

A33: for a being object st a in dom H holds

H . a is Ordinal

proof

thus A34:
H is one-to-one
:: thesis: for b
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;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

( ( not [b

proof

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 ) )
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 A33, A35;

R |_2 (R -Seg b), RelIncl B are_isomorphic by A10, A36, A37;

then A38: RelIncl B,R |_2 (R -Seg b) are_isomorphic by WELLORD1:40;

R |_2 (R -Seg a), RelIncl B are_isomorphic by A10, A35;

then R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A38, WELLORD1:42;

hence a = b by A1, A10, A35, A36, WELLORD1:47; :: thesis: verum

end;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 A33, A35;

R |_2 (R -Seg b), RelIncl B are_isomorphic by A10, A36, A37;

then A38: RelIncl B,R |_2 (R -Seg b) are_isomorphic by WELLORD1:40;

R |_2 (R -Seg a), RelIncl B are_isomorphic by A10, A35;

then R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A38, WELLORD1:42;

hence a = b by A1, A10, A35, A36, WELLORD1:47; :: thesis: verum

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

assume that
set Z = R -Seg b;

set P = R |_2 (R -Seg b);

A39: ( A = field (RelIncl A) & R |_2 (R -Seg b) is well-ordering ) by A1, Def1, WELLORD1:25;

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 A10, A33;

A42: R |_2 (R -Seg b), RelIncl B9 are_isomorphic by A10, A41;

A43: A9 in A by A10, A41, FUNCT_1:def 3;

A44: B9 in A by A10, A41, FUNCT_1:def 3;

A45: R |_2 (R -Seg a), RelIncl A9 are_isomorphic by A10, A41;

end;set P = R |_2 (R -Seg b);

A39: ( A = field (RelIncl A) & R |_2 (R -Seg b) is well-ordering ) by A1, Def1, WELLORD1:25;

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 A10, A33;

A42: R |_2 (R -Seg b), RelIncl B9 are_isomorphic by A10, A41;

A43: A9 in A by A10, A41, FUNCT_1:def 3;

A44: B9 in A by A10, A41, FUNCT_1:def 3;

A45: R |_2 (R -Seg a), RelIncl A9 are_isomorphic by A10, A41;

now :: thesis: ( a <> b implies [A9,B9] in RelIncl A )

hence
[(H . a),(H . b)] in RelIncl A
by A43, Def1; :: thesis: verumassume
a <> b
; :: thesis: [A9,B9] in RelIncl A

then A46: a in R -Seg b by A40, WELLORD1:1;

then A47: (R |_2 (R -Seg b)) -Seg a = R -Seg a by A1, WELLORD1:27;

R -Seg b c= field R by WELLORD1:9;

then A48: a in field (R |_2 (R -Seg b)) by A1, A46, WELLORD1:31;

A9 c= A by A43, ORDINAL1:def 2;

then A49: (RelIncl A) |_2 A9 = RelIncl A9 by Th1;

( A9 = (RelIncl A) -Seg A9 & R -Seg a c= R -Seg b ) by A1, A40, A41, A43, Th3, WELLORD1:29;

then A50: (R |_2 (R -Seg b)) |_2 ((R |_2 (R -Seg b)) -Seg a),(RelIncl A) |_2 ((RelIncl A) -Seg A9) are_isomorphic by A45, A49, A47, WELLORD1:22;

( B9 = (RelIncl A) -Seg B9 & B9 c= A ) by A44, Th3, ORDINAL1:def 2;

then R |_2 (R -Seg b),(RelIncl A) |_2 ((RelIncl A) -Seg B9) are_isomorphic by A42, Th1;

hence [A9,B9] in RelIncl A by A43, A44, A39, A48, A50, WELLORD1:51; :: thesis: verum

end;then A46: a in R -Seg b by A40, WELLORD1:1;

then A47: (R |_2 (R -Seg b)) -Seg a = R -Seg a by A1, WELLORD1:27;

R -Seg b c= field R by WELLORD1:9;

then A48: a in field (R |_2 (R -Seg b)) by A1, A46, WELLORD1:31;

A9 c= A by A43, ORDINAL1:def 2;

then A49: (RelIncl A) |_2 A9 = RelIncl A9 by Th1;

( A9 = (RelIncl A) -Seg A9 & R -Seg a c= R -Seg b ) by A1, A40, A41, A43, Th3, WELLORD1:29;

then A50: (R |_2 (R -Seg b)) |_2 ((R |_2 (R -Seg b)) -Seg a),(RelIncl A) |_2 ((RelIncl A) -Seg A9) are_isomorphic by A45, A49, A47, WELLORD1:22;

( B9 = (RelIncl A) -Seg B9 & B9 c= A ) by A44, Th3, ORDINAL1:def 2;

then R |_2 (R -Seg b),(RelIncl A) |_2 ((RelIncl A) -Seg B9) are_isomorphic by A42, Th1;

hence [A9,B9] in RelIncl A by A43, A44, A39, A48, A50, WELLORD1:51; :: thesis: verum

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 A1, RELAT_2:def 9;

then A55: a <> b by A51, A54;

R is_connected_in field R by A1, RELAT_2:def 14;

then A56: [b,a] in R by A51, A52, A54, A55;

then A57: R -Seg b c= R -Seg a by A1, A51, A52, WELLORD1:29;

A58: RelIncl A is_antisymmetric_in field (RelIncl A) by RELAT_2:def 12;

A59: A = field (RelIncl A) 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 A10, A51;

A61: R |_2 (R -Seg b), RelIncl B9 are_isomorphic by A10, A52;

A62: B9 in A by A10, A52, FUNCT_1:def 3;

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 A10, A51, FUNCT_1:def 3;

then ( A9 = (RelIncl A) -Seg A9 & A9 c= A ) by Th3, ORDINAL1:def 2;

then A65: R |_2 (R -Seg a),(RelIncl A) |_2 ((RelIncl A) -Seg A9) are_isomorphic by A60, Th1;

A66: b in R -Seg a by A54, A56, WELLORD1:1;

then A67: (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, WELLORD1:27;

B9 = (RelIncl A) -Seg B9 by A62, Th3;

then A68: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),(RelIncl A) |_2 ((RelIncl A) -Seg B9) are_isomorphic by A61, A63, A67, A57, WELLORD1:22;

R -Seg a c= field R by WELLORD1:9;

then A69: b in field (R |_2 (R -Seg a)) by A1, A66, WELLORD1:31;

R |_2 (R -Seg a) is well-ordering by A1, WELLORD1:25;

then [B9,A9] in RelIncl A by A69, A64, A62, A59, A65, A68, WELLORD1:51;

then H . a = H . b by A53, A58, A64, A62, A59;

hence contradiction by A10, A34, A51, A52, A55; :: thesis: verum