TrivOrthoRelStr is Pure ;
hence ex b₁ being non empty OrthoRelStr st
( b₁ is Pure & b₁ is Dneg & b₁ is PartialOrdered & b₁ is strict ) ; :: thesis: verum