theorem Th7: :: TAXONOM1:7

for X being set
for R being Relation of X st R is_symmetric_in X holds
R [*] is_symmetric_in X