let O be non empty OrthoRelStr ; :: thesis: ( O is irreflexive & O is SubStrictPartialOrdered implies O is StrictPartialOrdered )
assume A1: ( O is irreflexive & O is SubStrictPartialOrdered ) ; :: thesis: O is StrictPartialOrdered
then ( O is asymmetric & O is SubTransitive ) by Def27;
hence O is StrictPartialOrdered by A1, Def28; :: thesis: verum