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:47;
then A1: (.: ((a .: ) ` )) "\/" (.: (a .: )) = Top B by LATTICE2:79;
((a .: ) ` ) "\/" (a .: ) = Top (B .: ) by LATTICES:48;
then (.: ((a .: ) ` )) "/\" (.: (a .: )) = Bottom B by LATTICE2:78;
then .: ((a .: ) ` ) is_a_complement_of a by A1, LATTICES:def 18;
hence (a .: ) ` = a ` by LATTICES:def 21; :: thesis: verum