theorem Th27: :: ROBBINS1:27

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 `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))