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 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
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 ;
then A8: R -Seg b c= R -Seg a by ;
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 ;
hence (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic by ; :: thesis: verum
end;
then ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic by ;
hence a in Z by A2, A3; :: thesis: verum
end;
then field R c= Z by ;
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 ; :: thesis: verum