theorem Th7: :: WELLORD2:13

for R being Relation st R is well-ordering holds
ex A being Ordinal st R, RelIncl A are_isomorphic