theorem :: OPOSET_1:2

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