:: deftheorem Def9 defines EqRelOf-like ORDERS_5:def 9 :
for A being Preorder
for R being Equivalence_Relation of the carrier of A holds
( R is EqRelOf-like iff R = EqRelOf A );