:: deftheorem Def6 defines EqRelOf ORDERS_5:def 6 :
for A being Preorder
for b₂ being Equivalence_Relation of the carrier of A holds
( b₂ = EqRelOf A iff for x, y being Element of A holds
( [x,y] in b₂ iff ( x <= y & y <= x ) ) );