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