set RO = the InternalRel of O;
X: field the InternalRel of O c= the carrier of O \/ the carrier of O by RELSET_1:19;
thus ( O is irreflexive implies the InternalRel of O is irreflexive ) :: thesis: ( the InternalRel of O is irreflexive implies O is irreflexive )

proof

assume Z: O is irreflexive ; :: thesis: the InternalRel of O is irreflexive
let x be set ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( not x in field the InternalRel of O or not [x,x] in the InternalRel of O )
assume x in field the InternalRel of O ; :: thesis: not [x,x] in the InternalRel of O
then x in the carrier of O by X;
hence not [x,x] in the InternalRel of O by Z, NECKLACE:def 6; :: thesis: verum

end;

assume Z: the InternalRel of O is_irreflexive_in field the InternalRel of O ; :: according to RELAT_2:def 10 :: thesis: O is irreflexive
let x be set ; :: according to NECKLACE:def 6 :: thesis: ( not x in the carrier of O or not [x,x] in the InternalRel of O )
assume x in the carrier of O ; :: thesis: not [x,x] in the InternalRel of O

per cases ( x in field the InternalRel of O or not x in field the InternalRel of O ) ;

suppose x in field the InternalRel of O ; :: thesis: not [x,x] in the InternalRel of O

hence not [x,x] in the InternalRel of O by Z, RELAT_2:def 2; :: thesis: verum

end;

suppose not x in field the InternalRel of O ; :: thesis: not [x,x] in the InternalRel of O

hence not [x,x] in the InternalRel of O by RELAT_1:30; :: thesis: verum

end;

end;