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)) `) = Bot L