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 Def16;
hence O is irreflexive by Th10; :: thesis: verum