:: deftheorem defines irreflexive OPOSET_1:def 6 :
for O being non empty RelStr holds
( O is irreflexive iff the InternalRel of O is_irreflexive_in the carrier of O );