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