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 & f is Orderinvolutive ) by OPOSET_1:def 33;
consider g being Function of L,L such that
A2: ( g = f & g is dneg & g is antitone ) by A1, OPOSET_1:def 32;
thus L is Dneg by A1, A2, OPOSET_1:def 6; :: thesis: verum