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