let R be Relation; ( R is well-ordering implies ex A being Ordinal st R, RelIncl A are_isomorphic )
assume A1:
R is well-ordering
; ex A being Ordinal st R, RelIncl A are_isomorphic
defpred S1[ 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 & S1[a] ) )
from XBOOLE_0:sch 1();
now for a being object st a in field R & R -Seg a c= Z holds
a in Zlet a be
object ;
( 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
;
a in Zset P =
R |_2 (R -Seg a);
now 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 ;
( 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))
;
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;
(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;
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;
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; verum