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 & f is dneg ) by OPOSET_1:def 6;
A2: f . x = x ` by A1, ROBBINS1:def 3;
f . (f . x) = x by A1, OPOSET_1:def 3;
hence (x ` ) ` = x by A1, A2, ROBBINS1:def 3; :: thesis: verum