let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for a, b, c being Element of L holds a *' (b + c) = (a *' b) + (a *' c)
let a, b, c be Element of L; :: thesis: a *' (b + c) = (a *' b) + (a *' c)
( ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = Top L & ((a *' b) + (a *' c)) *' ((a *' (b + c)) `) = Bot L ) by Th28, Th29;
then ((a *' b) + (a *' c)) ` = (a *' (b + c)) ` by Th23;
hence a *' (b + c) = (a *' b) + (a *' c) by Th10; :: thesis: verum