theorem Th2: :: SHEFFER1:2

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