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;
( f is V300() & f is antitone ) by A2, OPOSET_1:def 17;
hence L is Dneg by A1, OPOSET_1:def 3; :: thesis: verum