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₁[ 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₁[a] ) ) from XBOOLE_0:sch 1();

now :: thesis: for a being object st a in field R & R -Seg a c= Z holds
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);

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

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;

then ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic by A1, Th6, WELLORD1:25;
hence a in Z by A2, A3; :: thesis: verum

end;

then field R c= Z by A1, WELLORD1:33;
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