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