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