theorem Th6: :: WELLORD2:12

for R being Relation st R is well-ordering & ( for a being object st a in field R holds
ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic ) holds
ex A being Ordinal st R, RelIncl A are_isomorphic