:: deftheorem defines is_order_type_of WELLORD2:def 3 :
for A being Ordinal
for R being Relation holds
( A is_order_type_of R iff A = order_type_of R );