theorem :: PARTIT_2:23

for S, X being non empty set
for R being Relation of X st R is symmetric holds
R is_symmetric_in S