let O be non empty OrthoRelStr ; :: thesis: ( O is SubStrictPartialOrdered implies O is SubIrreFlexive )
assume O is SubStrictPartialOrdered ; :: thesis: O is SubIrreFlexive
then ( O is asymmetric & O is SubTransitive ) by Def27;
hence O is SubIrreFlexive by Th37; :: thesis: verum