theorem Th5: :: SHEFFER1:5

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr
for x being Element of L holds x "/\" (Bot' L) = Bot' L