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)) `) = Top L
let a, b, c be Element of L; :: thesis: ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = Top L
set A = (a *' b) *' c;
set B = (a *' b) *' (c `);
set C = (a *' (b `)) *' c;
set D = (a *' (b `)) *' (c `);
set E = ((a `) *' b) *' c;
set F = ((a `) *' b) *' (c `);
set G = ((a `) *' (b `)) *' c;
set H = ((a `) *' (b `)) *' (c `);
set ABC = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c);
set GH = (((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `));
( (a *' (b + c)) ` = (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) & (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c) ) by Th26, Th27;
then ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = ((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + (((((a *' (b `)) *' (c `)) + (((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 `)) + (((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 `)) + (((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 `))) + (((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 `))) + ((((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 `))) + ((((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 `))) + (((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 `))) + (((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 `))) + (((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 `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) by LATTICES:def 5
.= Top L by Th24 ;
hence ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = Top L ; :: thesis: verum