theorem Th14: :: OPOSET_1:14

the Compl of TrivOrthoRelStr is Orderinvolutive