let L be non empty join-commutative join-associative Huntington ComplLattStr ; :: 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);
A1: ((a *' (b ` )) *' c) *' ((a *' (b ` )) *' (c ` )) = Bot L by Th26;
A2: ( ((a *' b) *' c) *' (((a ` ) *' (b ` )) *' c) = Bot L & ((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` )) = Bot L & ((a *' (b ` )) *' c) *' (((a ` ) *' b) *' c) = Bot L ) by Th26;
A3: (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)) = (Bot L) + (((a *' b) *' c) *' (((a ` ) *' b) *' c)) by Th26
.= (Bot L) + (Bot L) by Th26
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' b) *' c) *' (((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c))) ` ) by Th29
.= (((a *' b) *' c) *' (((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c))) ` by Th14 ;
then Bot L = ((((a *' b) *' c) *' (((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c))) ` ) ` by Th10
.= ((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 Th26
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' b) *' c) *' ((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` )))) ` ) by Th29
.= (((a *' b) *' c) *' ((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` )))) ` by Th14 ;
then Bot L = ((((a *' b) *' c) *' ((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` )))) ` ) ` by Th10
.= ((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 by A2, Def7;
then Top L = (Bot L) + ((((a *' b) *' c) *' (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c))) ` ) by Th29
.= (((a *' b) *' c) *' (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c))) ` by Th14 ;
then Bot L = ((((a *' b) *' c) *' (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c))) ` ) ` by Th10
.= ((a *' b) *' c) *' (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) by Th3 ;
then A4: (((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 Th26
.= Bot L by Def7 ;
(((a *' b) *' (c ` )) *' ((a *' (b ` )) *' (c ` ))) + (((a *' b) *' (c ` )) *' (((a ` ) *' b) *' c)) = (Bot L) + (((a *' b) *' (c ` )) *' (((a ` ) *' b) *' c)) by Th26
.= (Bot L) + (Bot L) by Th26
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' b) *' (c ` )) *' (((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c))) ` ) by Th29
.= (((a *' b) *' (c ` )) *' (((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c))) ` by Th14 ;
then Bot L = ((((a *' b) *' (c ` )) *' (((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c))) ` ) ` by Th10
.= ((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 Th26
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' b) *' (c ` )) *' ((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` )))) ` ) by Th29
.= (((a *' b) *' (c ` )) *' ((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` )))) ` by Th14 ;
then Bot L = ((((a *' b) *' (c ` )) *' ((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` )))) ` ) ` by Th10
.= ((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 Th26
.= 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 Th29
.= (((a *' b) *' (c ` )) *' (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c))) ` by Th14 ;
then Bot L = ((((a *' b) *' (c ` )) *' (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c))) ` ) ` by Th10
.= ((a *' b) *' (c ` )) *' (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) by Th3 ;
then A5: (((a *' b) *' (c ` )) *' (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c))) + (((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` ))) = Bot L by A2, Def7;
A6: Top L = (Bot L) + ((((a *' b) *' c) *' ((((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` )))) ` ) by A4, Th29
.= (((a *' b) *' c) *' ((((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` )))) ` by Th14 ;
A7: Top L = (Bot L) + ((((a *' b) *' (c ` )) *' ((((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` )))) ` ) by A5, Th29
.= (((a *' b) *' (c ` )) *' ((((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` )))) ` by Th14 ;
(((a *' (b ` )) *' c) *' ((a *' (b ` )) *' (c ` ))) + (((a *' (b ` )) *' c) *' (((a ` ) *' b) *' c)) = (Bot L) + (Bot L) by A1, Th26
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' (b ` )) *' c) *' (((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c))) ` ) by Th29
.= (((a *' (b ` )) *' c) *' (((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c))) ` by Th14 ;
then Bot L = ((((a *' (b ` )) *' c) *' (((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c))) ` ) ` by Th10
.= ((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 Th26
.= Bot L by Def7 ;
then Top L = (Bot L) + ((((a *' (b ` )) *' c) *' ((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` )))) ` ) by Th29
.= (((a *' (b ` )) *' c) *' ((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` )))) ` by Th14 ;
then Bot L = ((((a *' (b ` )) *' c) *' ((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` )))) ` ) ` by Th10
.= ((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 Th26
.= 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 Th29
.= (((a *' (b ` )) *' c) *' (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c))) ` by Th14 ;
then Bot L = ((((a *' (b ` )) *' c) *' (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c))) ` ) ` by Th10
.= ((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 Th26
.= Bot L by Def7 ;
then A8: Top L = (Bot L) + ((((a *' (b ` )) *' c) *' ((((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` )))) ` ) by Th29
.= (((a *' (b ` )) *' c) *' ((((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` )))) ` by Th14 ;
A9: ((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 A6, Th10 ;
A10: ((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 A7, Th10 ;
A11: ((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 A8, Th10 ;
(((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 A9, A10, 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 Th29
.= ((((a *' b) *' c) + ((a *' b) *' (c ` ))) *' ((((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` )))) ` by Th14 ;
then Bot L = (((((a *' b) *' c) + ((a *' b) *' (c ` ))) *' ((((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` )))) ` ) ` by Th10
.= (((a *' b) *' c) + ((a *' b) *' (c ` ))) *' ((((((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 ` )))) + (((a *' (b ` )) *' c) *' ((((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` )))) = Bot L by A11, 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 Th29
.= (((((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 Th14 ;
then 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 Th10
.= ((((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 ;
hence ((a *' b) + (a *' c)) *' ((a *' (b + c)) ` ) = Bot L by A3, Th27; :: thesis: verum