theorem Th1: :: ROBBINS1:1

for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b being Element of L holds (a *' b) + (a *' (b `)) = a by Def6;