let S be full SubRelStr of L; :: thesis: S is symmetric
A1: ( the carrier of S c= the carrier of L & the InternalRel of S = the InternalRel of L |_2 the carrier of S ) by YELLOW_0:def 13, YELLOW_0:def 14;
let x, y be set ; :: according to NECKLACE:def 4,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 A2: ( x in the carrier of S & y in the carrier of S & [x,y] in the InternalRel of S ) ; :: thesis: [y,x] in the InternalRel of S
then A3: ( x in the carrier of L & y in the carrier of L & [x,y] in the InternalRel of L ) by A1, XBOOLE_0:def 4;
the InternalRel of L is_symmetric_in the carrier of L by NECKLACE:def 4;
then A4: [y,x] in the InternalRel of L by A3, RELAT_2:def 3;
[y,x] in [:the carrier of S,the carrier of S:] by A2, ZFMISC_1:106;
hence [y,x] in the InternalRel of S by A1, A4, XBOOLE_0:def 4; :: thesis: verum