set R = {[0,0]};

{[0,0]} c= [:{0},{0}:] by ZFMISC_1:29;

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 3 :: thesis: verum

{[0,0]} c= [:{0},{0}:] by ZFMISC_1:29;

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 3 :: thesis: verum

proof

let x, y be object ; :: 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:28;

then [y,x] in [:{0},{0}:] by ZFMISC_1:28;

hence [y,x] in the InternalRel of S by ZFMISC_1:29; :: thesis: verum

end;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:28;

then [y,x] in [:{0},{0}:] by ZFMISC_1:28;

hence [y,x] in the InternalRel of S by ZFMISC_1:29; :: thesis: verum