let L be non empty join-commutative join-associative Huntington ComplLLattStr ; for a, b, c being Element of L holds ((((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) = Top L
let a, b, c be Element of L; ((((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' 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 `);
((((((((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 *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))
by Def6
.=
(((((a *' b) + (((a *' (b `)) *' c) + ((a *' (b `)) *' (c `)))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))
by LATTICES:def 5
.=
(((((a *' b) + (a *' (b `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))
by Def6
.=
((((a *' b) + (a *' (b `))) + ((((a `) *' b) *' c) + (((a `) *' b) *' (c `)))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))
by LATTICES:def 5
.=
((((a *' b) + (a *' (b `))) + ((a `) *' b)) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))
by Def6
.=
(((a *' b) + (a *' (b `))) + ((a `) *' b)) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `)))
by LATTICES:def 5
.=
(((a *' b) + (a *' (b `))) + ((a `) *' b)) + ((a `) *' (b `))
by Def6
.=
(a + ((a `) *' b)) + ((a `) *' (b `))
by Def6
.=
a + (((a `) *' b) + ((a `) *' (b `)))
by LATTICES:def 5
.=
a + (a `)
by Def6
;
hence
((((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) = Top L
by Def8; verum