theorem Th4: :: ROBBINS1:4

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