let R be Relation; :: thesis: ( R is well-ordering implies ex A being Ordinal st R, RelIncl A are_isomorphic )

assume A1: R is well-ordering ; :: thesis: ex A being Ordinal st R, RelIncl A are_isomorphic

defpred S_{1}[ object ] means ex A being Ordinal st R |_2 (R -Seg $1), RelIncl A are_isomorphic ;

consider Z being set such that

A2: for a being object holds

( a in Z iff ( a in field R & S_{1}[a] ) )
from XBOOLE_0:sch 1();

then for a being object st a in field R holds

ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic by A2;

hence ex A being Ordinal st R, RelIncl A are_isomorphic by A1, Th6; :: thesis: verum

assume A1: R is well-ordering ; :: thesis: ex A being Ordinal st R, RelIncl A are_isomorphic

defpred S

consider Z being set such that

A2: for a being object holds

( a in Z iff ( a in field R & S

now :: thesis: for a being object st a in field R & R -Seg a c= Z holds

a in Z

then
field R c= Z
by A1, WELLORD1:33;a in Z

let a be object ; :: thesis: ( a in field R & R -Seg a c= Z implies a in Z )

assume that

A3: a in field R and

A4: R -Seg a c= Z ; :: thesis: a in Z

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

hence a in Z by A2, A3; :: thesis: verum

end;assume that

A3: a in field R and

A4: R -Seg a c= Z ; :: thesis: a in Z

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

now :: thesis: for b being object st b in field (R |_2 (R -Seg a)) holds

ex A being Ordinal st (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic

then
ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic
by A1, Th6, WELLORD1:25;ex A being Ordinal st (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic

let b be object ; :: thesis: ( b in field (R |_2 (R -Seg a)) implies ex A being Ordinal st (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic )

assume A5: b in field (R |_2 (R -Seg a)) ; :: thesis: ex A being Ordinal st (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic

then A6: b in R -Seg a by WELLORD1:12;

then A7: [b,a] in R by WELLORD1:1;

b in field R by A5, WELLORD1:12;

then A8: R -Seg b c= R -Seg a by A1, A3, A7, WELLORD1:29;

consider A being Ordinal such that

A9: R |_2 (R -Seg b), RelIncl A are_isomorphic by A2, A4, A6;

take A = A; :: thesis: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic

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

hence (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic by A9, A8, WELLORD1:22; :: thesis: verum

end;assume A5: b in field (R |_2 (R -Seg a)) ; :: thesis: ex A being Ordinal st (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic

then A6: b in R -Seg a by WELLORD1:12;

then A7: [b,a] in R by WELLORD1:1;

b in field R by A5, WELLORD1:12;

then A8: R -Seg b c= R -Seg a by A1, A3, A7, WELLORD1:29;

consider A being Ordinal such that

A9: R |_2 (R -Seg b), RelIncl A are_isomorphic by A2, A4, A6;

take A = A; :: thesis: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic

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

hence (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic by A9, A8, WELLORD1:22; :: thesis: verum

hence a in Z by A2, A3; :: thesis: verum

then for a being object st a in field R holds

ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic by A2;

hence ex A being Ordinal st R, RelIncl A are_isomorphic by A1, Th6; :: thesis: verum