theorem Th5: :: NECKLA_3:5

for X being 1 -element set
for R being Relation of X holds R is_symmetric_in X