:: deftheorem defines well-ordering WELLORD1:def 4 :
for R being Relation holds
( R is well-ordering iff ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded ) );