:: deftheorem Def2 defines "\/" EQREL_1:def 2 :
for X being set
for EqR1, EqR2, b₄ being Equivalence_Relation of X holds
( b₄ = EqR1 "\/" EqR2 iff ( EqR1 \/ EqR2 c= b₄ & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b₄ c= EqR ) ) );