let L be non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr ; :: thesis: for x being Element of L holds x "/\" (x `#) = Bot' L
let x be Element of L; :: thesis: x "/\" (x `#) = Bot' L
x `# is_a_complement'_of x by Def8;
hence x "/\" (x `#) = Bot' L ; :: thesis: verum