let O be non empty RelStr ; :: thesis: ( O is reflexive implies O is SubReFlexive )
set RO = the InternalRel of O;
assume O is reflexive ; :: thesis: O is SubReFlexive
then the InternalRel of O is_reflexive_in the carrier of O by ORDERS_2:def 2;
then the InternalRel of O is reflexive by PARTIT_2:21;
hence O is SubReFlexive by Def9; :: thesis: verum