:: deftheorem defines well_orders WELLORD1:def 5 :
for R being Relation
for X being set holds
( R well_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X ) );