let S be full SubRelStr of L; :: thesis: S is irreflexive
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 be set ; :: according to NECKLACE:def 6 :: thesis: ( not x in the carrier of S or not [x,x] in the InternalRel of S )
assume x in the carrier of S ; :: thesis: not [x,x] in the InternalRel of S
then not [x,x] in the InternalRel of L by A1, NECKLACE:def 6;
hence not [x,x] in the InternalRel of S by A1, XBOOLE_0:def 4; :: thesis: verum