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

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