theorem Th30: :: ROBBINS1:30

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