TrivAsymOrthoRelStr is StrictPartialOrdered ;
hence ex b₁ being non empty strict OrthoRelStr st
( b₁ is irreflexive & b₁ is StrictPartialOrdered ) ; :: thesis: verum