let O be non empty OrthoRelStr ; :: thesis: ( O is StrictPartialOrdered implies O is SubStrictPartialOrdered )
assume O is StrictPartialOrdered ; :: thesis: O is SubStrictPartialOrdered
then ( O is Asymmetric & O is transitive ) by Def28;
hence O is SubStrictPartialOrdered by Def27; :: thesis: verum