let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; :: thesis: for x being Element of L holds x "/\" (Bot' L) = Bot' L
let x be Element of L; :: thesis: x "/\" (Bot' L) = Bot' L
x "/\" (Bot' L) = (x "/\" (Bot' L)) "\/" (Bot' L) by Def4
.= (x "/\" (Bot' L)) "\/" (x "/\" (x `# )) by Th4
.= x "/\" ((Bot' L) "\/" (x `# )) by LATTICES:def 11
.= x "/\" (x `# ) by Def4
.= Bot' L by Th4 ;
hence x "/\" (Bot' L) = Bot' L ; :: thesis: verum