theorem :: EQREL_1:14

for X being set
for EqR being Equivalence_Relation of X holds EqR "\/" EqR = EqR ;