set R = CompleteRelStr n;
set cR = the carrier of (CompleteRelStr n);
set iR = the InternalRel of (CompleteRelStr n);
A1: the carrier of (CompleteRelStr n) = n by Def7;
thus CompleteRelStr n is irreflexive by A1, Th32; :: thesis: CompleteRelStr n is symmetric
thus CompleteRelStr n is symmetric :: thesis: verum

proof

let x, y be object ; :: according to RELAT_2:def 3,NECKLACE:def 3 :: thesis: ( not x in the carrier of (CompleteRelStr n) or not y in the carrier of (CompleteRelStr n) or not [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
assume ( x in the carrier of (CompleteRelStr n) & y in the carrier of (CompleteRelStr n) ) ; :: thesis: ( not [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
then A2: ( x in n & y in n ) by Def7;
assume [x,y] in the InternalRel of (CompleteRelStr n) ; :: thesis: [y,x] in the InternalRel of (CompleteRelStr n)
hence [y,x] in the InternalRel of (CompleteRelStr n) by A2, Th32; :: thesis: verum

end;