theorem Th26: :: ROBBINS1:26

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