:: deftheorem Def1 defines EqCl MSUALG_5:def 1 :
for X being set
for R being Relation of X
for b₃ being Equivalence_Relation of X holds
( b₃ = EqCl R iff ( R c= b₃ & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b₃ c= EqR2 ) ) );