:: deftheorem defines quasi_orders ORDERS_1:def 7 :
for R being Relation
for X being set holds
( R quasi_orders X iff ( R is_reflexive_in X & R is_transitive_in X ) );