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 LNRS;
thus CompleteRelStr n is irreflexive :: thesis: CompleteRelStr n is symmetric

proof

let x be set ; :: according to NECKLACE:def 6 :: thesis: ( not x in the carrier of (CompleteRelStr n) or not [x,x] in the InternalRel of (CompleteRelStr n) )
assume x in the carrier of (CompleteRelStr n) ; :: thesis: not [x,x] in the InternalRel of (CompleteRelStr n)
hence not [x,x] in the InternalRel of (CompleteRelStr n) by A1, CRS; :: thesis: verum

end;

thus CompleteRelStr n is symmetric :: thesis: verum

proof

let x, y be set ; :: according to RELAT_2:def 3,NECKLACE:def 4 :: 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 A: ( x in n & y in n ) by LNRS;
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 A, CRS; :: thesis: verum

end;