theorem Th9: :: TAXONOM1:9

for X being non empty set
for R being Relation of X st R is_reflexive_in X & R is_symmetric_in X holds
R [*] is Equivalence_Relation of X