let L be distributive well-complemented preOrthoLattice; :: thesis: for x being Element of L holds (x ` ) ` = x
let x be Element of L; :: thesis: (x ` ) ` = x
A1: x ` is_a_complement_of x by Def10;
(x ` ) ` is_a_complement_of x ` by Def10;
then A2: ( ((x ` ) ` ) + (x ` ) = Top L & ((x ` ) ` ) "/\" (x ` ) = Bottom L ) by LATTICES:def 18;
( (x ` ) "\/" x = Top L & (x ` ) "/\" x = Bottom L ) by A1, LATTICES:def 18;
hence (x ` ) ` = x by A2, LATTICES:32; :: thesis: verum