let O be non empty OrthoRelStr ; :: thesis: ( O is StrictPartialOrdered implies O is irreflexive )
assume O is StrictPartialOrdered ; :: thesis: O is irreflexive
then ( O is asymmetric & O is transitive ) by Def28;
hence O is irreflexive by Th36; :: thesis: verum