theorem Th5: :: ROBBINS1:5

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ex c being Element of L st
for a being Element of L holds
( c + a = c & a + (a `) = c )