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