for R being Relation st R is well-ordering holds
field R, order_type_of R are_equipotent