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)) `) = Bot L
let a, b, c be Element of L; :: thesis: ((a *' b) + (a *' c)) *' ((a *' (b + c)) `) = Bot 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 DEFG = ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c);
(((a *' b) *' c) *' ((a *' (b `)) *' (c `))) + (((a *' b) *' c) *' (((a `) *' b) *' c)) = (Bot L) + (((a *' b) *' c) *' (((a `) *' b) *' c)) by Th25
.= (Bot L) + (Bot L) by Th25
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' b) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) by Th28
.= (((a *' b) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) ` by Th13 ;
then Bot L = ((((a *' b) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) ` by Th9
.= ((a *' b) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) by Th3 ;
then (((a *' b) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) + (((a *' b) *' c) *' (((a `) *' b) *' (c `))) = (Bot L) + (Bot L) by Th25
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' b) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) by Th28
.= (((a *' b) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) ` by Th13 ;
then A1: Bot L = ((((a *' b) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) ` by Th9
.= ((a *' b) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) by Th3 ;
((a *' b) *' c) *' (((a `) *' (b `)) *' c) = Bot L by Th25;
then (((a *' b) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) + (((a *' b) *' c) *' (((a `) *' (b `)) *' c)) = Bot L by A1, Def7;
then Top L = (Bot L) + ((((a *' b) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) by Th28
.= (((a *' b) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) ` by Th13 ;
then Bot L = ((((a *' b) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) ` by Th9
.= ((a *' b) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) by Th3 ;
then (((a *' b) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) + (((a *' b) *' c) *' (((a `) *' (b `)) *' (c `))) = (Bot L) + (Bot L) by Th25
.= Bot L by Def7 ;
then A2: Top L = (Bot L) + ((((a *' b) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) by Th28
.= (((a *' b) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) ` by Th13 ;
(((a *' b) *' (c `)) *' ((a *' (b `)) *' (c `))) + (((a *' b) *' (c `)) *' (((a `) *' b) *' c)) = (Bot L) + (((a *' b) *' (c `)) *' (((a `) *' b) *' c)) by Th25
.= (Bot L) + (Bot L) by Th25
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' b) *' (c `)) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) by Th28
.= (((a *' b) *' (c `)) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) ` by Th13 ;
then Bot L = ((((a *' b) *' (c `)) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) ` by Th9
.= ((a *' b) *' (c `)) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) by Th3 ;
then (((a *' b) *' (c `)) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) + (((a *' b) *' (c `)) *' (((a `) *' b) *' (c `))) = (Bot L) + (Bot L) by Th25
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' b) *' (c `)) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) by Th28
.= (((a *' b) *' (c `)) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) ` by Th13 ;
then Bot L = ((((a *' b) *' (c `)) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) ` by Th9
.= ((a *' b) *' (c `)) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) by Th3 ;
then (((a *' b) *' (c `)) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) + (((a *' b) *' (c `)) *' (((a `) *' (b `)) *' c)) = (Bot L) + (Bot L) by Th25
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' b) *' (c `)) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) by Th28
.= (((a *' b) *' (c `)) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) ` by Th13 ;
then A3: Bot L = ((((a *' b) *' (c `)) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) ` by Th9
.= ((a *' b) *' (c `)) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) by Th3 ;
((a *' (b `)) *' c) *' ((a *' (b `)) *' (c `)) = Bot L by Th25;
then (((a *' (b `)) *' c) *' ((a *' (b `)) *' (c `))) + (((a *' (b `)) *' c) *' (((a `) *' b) *' c)) = (Bot L) + (Bot L) by Th25
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' (b `)) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) by Th28
.= (((a *' (b `)) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) ` by Th13 ;
then Bot L = ((((a *' (b `)) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) ` by Th9
.= ((a *' (b `)) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) by Th3 ;
then (((a *' (b `)) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) + (((a *' (b `)) *' c) *' (((a `) *' b) *' (c `))) = (Bot L) + (Bot L) by Th25
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' (b `)) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) by Th28
.= (((a *' (b `)) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) ` by Th13 ;
then Bot L = ((((a *' (b `)) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) ` by Th9
.= ((a *' (b `)) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) by Th3 ;
then (((a *' (b `)) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) + (((a *' (b `)) *' c) *' (((a `) *' (b `)) *' c)) = (Bot L) + (Bot L) by Th25
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' (b `)) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) by Th28
.= (((a *' (b `)) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) ` by Th13 ;
then Bot L = ((((a *' (b `)) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) ` by Th9
.= ((a *' (b `)) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) by Th3 ;
then (((a *' (b `)) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) + (((a *' (b `)) *' c) *' (((a `) *' (b `)) *' (c `))) = (Bot L) + (Bot L) by Th25
.= Bot L by Def7 ;
then A4: Top L = (Bot L) + ((((a *' (b `)) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) by Th28
.= (((a *' (b `)) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) ` by Th13 ;
((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = Bot L by Th25;
then (((a *' b) *' (c `)) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) + (((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `))) = Bot L by A3, Def7;
then A5: Top L = (Bot L) + ((((a *' b) *' (c `)) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) by Th28
.= (((a *' b) *' (c `)) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) ` by Th13 ;
A6: ((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) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) ` by Th3
.= Bot L by A5, Th9 ;
((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) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) ` by Th3
.= Bot L by A2, Th9 ;
then (((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) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) = Bot L by A6, Def7;
then Top L = (Bot L) + (((((a *' b) *' c) + ((a *' b) *' (c `))) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) by Th28
.= ((((a *' b) *' c) + ((a *' b) *' (c `))) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) ` by Th13 ;
then A7: Bot L = (((((a *' b) *' c) + ((a *' b) *' (c `))) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) ` by Th9
.= (((a *' b) *' c) + ((a *' b) *' (c `))) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))) by Th3 ;
((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) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) ` by Th3
.= Bot L by A4, Th9 ;
then ((((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) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) = Bot L by A7, Def7;
then Top L = (Bot 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 `)))) `) by Th28
.= (((((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 Th13 ;
then A8: Bot 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 `)))) `) ` by Th9
.= ((((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 Th3 ;
(a *' (b + c)) ` = (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) by Th27;
hence ((a *' b) + (a *' c)) *' ((a *' (b + c)) `) = Bot L by A8, Th26; :: thesis: verum