:: deftheorem Def4 defines SubReFlexive OPOSET_1:def 4 :
for O being non empty RelStr holds
( O is SubReFlexive iff the InternalRel of O is reflexive );