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