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