let O be non empty RelStr ; :: thesis: ( O is symmetric & O is transitive implies O is SubReFlexive )
set R = the InternalRel of O;
assume ( O is symmetric & O is transitive ) ; :: 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