:: deftheorem Def5 defines EqRelOf ORDERS_5:def 5 :
for A being set
for D being a_partition of A
for b₃ being Equivalence_Relation of A holds
( b₃ = EqRelOf D iff D = Class b₃ );