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 Th3

.= x "/\" ((Bot' L) "\/" (x `#)) by LATTICES:def 11

.= x "/\" (x `#) by Def4

.= Bot' L by Th3 ;

hence x "/\" (Bot' L) = Bot' L ; :: thesis: verum

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 Th3

.= x "/\" ((Bot' L) "\/" (x `#)) by LATTICES:def 11

.= x "/\" (x `#) by Def4

.= Bot' L by Th3 ;

hence x "/\" (Bot' L) = Bot' L ; :: thesis: verum