let L be non empty join-commutative join-associative Huntington ComplLattStr ; :: 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)
A1: ((a *' b) + (a *' c)) + ((a *' (b + c)) ` ) = Top L by Th29;
((a *' b) + (a *' c)) *' ((a *' (b + c)) ` ) = Bot L by Th30;
then ((a *' b) + (a *' c)) ` = (a *' (b + c)) ` by A1, Th24;
hence a *' (b + c) = (a *' b) + (a *' c) by Th11; :: thesis: verum