let L be B_Lattice; :: thesis: for a being Element of L holds (a ` ) ` = a
let a be Element of L; :: thesis: (a ` ) ` = a
(a ` ) ` is_a_complement_of a ` by Def21;
then A1: ( ((a ` ) ` ) "\/" (a ` ) = Top L & ((a ` ) ` ) "/\" (a ` ) = Bottom L ) by Def18;
a ` is_a_complement_of a by Def21;
then ( a "\/" (a ` ) = Top L & a "/\" (a ` ) = Bottom L ) by Def18;
hence (a ` ) ` = a by A1, Th32; :: thesis: verum