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