let B be B_Lattice; :: thesis: for a being Element of B holds (a .:) ` = a `
let a be Element of B; :: thesis: (a .:) ` = a `
((a .:) `) "/\" (a .:) = Bottom (B .:) by LATTICES:20;
then A1: (.: ((a .:) `)) "\/" (.: (a .:)) = Top B by LATTICE2:62;
((a .:) `) "\/" (a .:) = Top (B .:) by LATTICES:21;
then (.: ((a .:) `)) "/\" (.: (a .:)) = Bottom B by LATTICE2:61;
then .: ((a .:) `) is_a_complement_of a by A1;
hence (a .:) ` = a ` by LATTICES:def 21; :: thesis: verum