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