thus ( O is irreflexive implies the InternalRel of O is_irreflexive_in the carrier of O ) :: thesis: ( the InternalRel of O is_irreflexive_in the carrier of O implies O is irreflexive )

proof

assume O is irreflexive ; :: thesis: the InternalRel of O is_irreflexive_in the carrier of O
then for x being set st x in the carrier of O holds
not [x,x] in the InternalRel of O by NECKLACE:def 5;
hence the InternalRel of O is_irreflexive_in the carrier of O by RELAT_2:def 2; :: thesis: verum

end;

assume the InternalRel of O is_irreflexive_in the carrier of O ; :: thesis: O is irreflexive
then for x being set st x in the carrier of O holds
not [x,x] in the InternalRel of O by RELAT_2:def 2;
hence O is irreflexive by NECKLACE:def 5; :: thesis: verum