let S be full SubRelStr of L; :: thesis: S is irreflexive

let x be set ; :: according to NECKLACE:def 5 :: thesis: ( not x in the carrier of S or not [x,x] in the InternalRel of S )

assume A1: x in the carrier of S ; :: thesis: not [x,x] in the InternalRel of S

the carrier of S c= the carrier of L by YELLOW_0:def 13;

then ( the InternalRel of S = the InternalRel of L |_2 the carrier of S & not [x,x] in the InternalRel of L ) by A1, NECKLACE:def 5, YELLOW_0:def 14;

hence not [x,x] in the InternalRel of S by XBOOLE_0:def 4; :: thesis: verum

let x be set ; :: according to NECKLACE:def 5 :: thesis: ( not x in the carrier of S or not [x,x] in the InternalRel of S )

assume A1: x in the carrier of S ; :: thesis: not [x,x] in the InternalRel of S

the carrier of S c= the carrier of L by YELLOW_0:def 13;

then ( the InternalRel of S = the InternalRel of L |_2 the carrier of S & not [x,x] in the InternalRel of L ) by A1, NECKLACE:def 5, YELLOW_0:def 14;

hence not [x,x] in the InternalRel of S by XBOOLE_0:def 4; :: thesis: verum