theorem :: NECKLA_3:34

for R being RelStr st R in fin_RelStr_sp holds
R is symmetric