theorem Th5: :: MYCIELSK:5

for R being symmetric RelStr
for x, y being set st x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R holds
[y,x] in the InternalRel of R by NECKLACE:def 3, RELAT_2:def 3;