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
(x ` ) ` is_a_complement_of x ` by Def10;
then A1: ( ((x ` ) ` ) + (x ` ) = Top L & ((x ` ) ` ) "/\" (x ` ) = Bottom L ) by LATTICES:def 18;
x ` is_a_complement_of x by Def10;
then ( (x ` ) "\/" x = Top L & (x ` ) "/\" x = Bottom L ) by LATTICES:def 18;
hence (x ` ) ` = x by A1, LATTICES:32; :: thesis: verum