let L be non empty Dneg OrthoRelStr ; :: thesis: for x being Element of L holds (x ` ) ` = x
let x be Element of L; :: thesis: (x ` ) ` = x
consider f being Function of L,L such that
A1: f = the Compl of L and
A2: f is dneg by OPOSET_1:def 6;
( f . x = x ` & f . (f . x) = x ) by A1, A2, OPOSET_1:def 3, ROBBINS1:def 3;
hence (x ` ) ` = x by A1, ROBBINS1:def 3; :: thesis: verum