theorem Th12: :: EQREL_1:12

for X being set
for R being Relation of X ex EqR being Equivalence_Relation of X st
( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )