:: deftheorem defines OrderInvolutive OPOSET_1:def 18 :
for PO being non empty OrthoRelStr holds
( PO is OrderInvolutive iff the Compl of PO is Orderinvolutive );