:: deftheorem defines quasi_ordered DICKSON:def 3 :
for R being RelStr holds
( R is quasi_ordered iff ( R is reflexive & R is transitive ) );