let O be non empty RelStr ; :: thesis: ( O is SubSymmetric & O is SubTransitive implies O is SubReFlexive )
set R = the InternalRel of O;
assume ( O is SubSymmetric & O is SubTransitive ) ; :: thesis: O is SubReFlexive
then ( the InternalRel of O is symmetric & the InternalRel of O is transitive ) by Def13, Def19;
hence O is SubReFlexive by Def9; :: thesis: verum