:: deftheorem Def3 defines Class EQREL_1:def 3 :
for X being set
for EqR being Equivalence_Relation of X
for b₃ being Subset-Family of X holds
( b₃ = Class EqR iff for A being Subset of X holds
( A in b₃ iff ex x being object st
( x in X & A = Class (EqR,x) ) ) );