:: deftheorem Def2 defines order_type_of WELLORD2:def 2 :
for R being Relation st R is well-ordering holds
for b₂ being Ordinal holds
( b₂ = order_type_of R iff R, RelIncl b₂ are_isomorphic );