let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for a, b, c being Element of L holds (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)
let a, b, c be Element of L; :: thesis: (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)
set A = (a *' b) *' c;
a *' c = ((a *' c) *' b) + ((a *' c) *' (b `)) by Def6
.= ((a *' b) *' c) + ((a *' c) *' (b `)) by Th16
.= ((a *' b) *' c) + ((a *' (b `)) *' c) by Th16 ;
hence (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + (((a *' b) *' c) + ((a *' (b `)) *' c)) by Def6
.= (((a *' b) *' c) + (((a *' b) *' (c `)) + ((a *' b) *' c))) + ((a *' (b `)) *' c) by LATTICES:def 5
.= ((((a *' b) *' c) + ((a *' b) *' c)) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c) by LATTICES:def 5
.= (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c) by Def7 ;
:: thesis: verum