theorem Th3: :: SHEFFER1:3

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