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₁[ set ] 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 set holds
( a in Z iff ( a in field R & S₁[a] ) ) from XBOOLE_0:sch 1();

now

let a be set ; :: thesis: ( a in field R & R -Seg a c= Z implies a in Z )
assume A3: ( a in field R & R -Seg a c= Z ) ; :: thesis: a in Z
set P = R |_2 (R -Seg a);
A4: R |_2 (R -Seg a) is well-ordering by A1, WELLORD1:32;

now

let b be set ; :: 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 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 A5: ( b in R -Seg a & b in field R ) by WELLORD1:19;
then consider A being Ordinal such that
A6: R |_2 (R -Seg b), RelIncl A are_isomorphic by A2, A3;
take A = A; :: thesis: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic
A7: (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, A3, A5, WELLORD1:35;
[b,a] in R by A5, WELLORD1:def 1;
then R -Seg b c= R -Seg a by A1, A3, A5, WELLORD1:37;
hence (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic by A6, A7, WELLORD1:29; :: thesis: verum

end;

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

end;

then field R c= Z by A1, WELLORD1:41;
then for a being set 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, Th13; :: thesis: verum