for X being set
for A being Ordinal st X,A are_equipotent holds
ex R being Order of X st
( R well_orders X & order_type_of R = A )