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
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;