for O being non empty RelStr st O is reflexive holds
O is SubReFlexive by PARTIT_2:21;