set R = {[0 ,0 ]};
{[0 ,0 ]} c= [:{0 },{0 }:] by ZFMISC_1:35;
then reconsider R = {[0 ,0 ]} as Relation of {0 } ;
take S = RelStr(# {0 },R #); :: thesis: ( not S is empty & S is symmetric )
thus not S is empty ; :: thesis: S is symmetric
thus the InternalRel of S is_symmetric_in the carrier of S :: according to NECKLACE:def 4 :: thesis: verum

proof

let x, y be set ; :: according to RELAT_2:def 3 :: thesis: ( not x in the carrier of S or not y in the carrier of S or not [x,y] in the InternalRel of S or [y,x] in the InternalRel of S )
assume that
x in the carrier of S and
y in the carrier of S and
A1: [x,y] in the InternalRel of S ; :: thesis: [y,x] in the InternalRel of S
( x = 0 & y = 0 ) by A1, ZFMISC_1:34;
then [y,x] in [:{0 },{0 }:] by ZFMISC_1:34;
hence [y,x] in the InternalRel of S by ZFMISC_1:35; :: thesis: verum

end;