let L be non empty PartialOrdered OrthoRelStr ; :: thesis: ( L is OrderInvolutive implies L is Dneg )
assume L is OrderInvolutive ; :: thesis: L is Dneg
then consider f being Function of L,L such that
A1: f = the Compl of L and
A2: f is Orderinvolutive by OPOSET_1:def 18;
ex g being Function of L,L st
( g = f & g is involutive & g is antitone ) by A2, OPOSET_1:def 17;
hence L is Dneg by A1, OPOSET_1:def 3; :: thesis: verum