TrivOrthoRelStr is QuasiPure by Def23;
hence ex b₁ being non empty OrthoRelStr st
( b₁ is QuasiPure & b₁ is Dneg & b₁ is QuasiOrdered & b₁ is strict ) ; :: thesis: verum