let L be non empty join-commutative join-associative Huntington ComplLLattStr ; 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; ((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 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 A1: 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
;
((a *' b) *' c) *' (((a ` ) *' (b ` )) *' c) = Bot L
by Th26;
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 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 A2: 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
;
(((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 A3: 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
;
((a *' (b ` )) *' c) *' ((a *' (b ` )) *' (c ` )) = Bot L
by Th26;
then (((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))) ` )
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 A4: 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
;
((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` )) = Bot L
by Th26;
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 Th29
.=
(((a *' b) *' (c ` )) *' ((((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` )))) `
by Th14
;
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, 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 ` )))) ` ) `
by Th3
.=
Bot L
by A2, Th10
;
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 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 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 Th10
.=
(((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, Th10
;
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 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 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 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
;
(a *' (b + c)) ` = (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` ))
by Th28;
hence
((a *' b) + (a *' c)) *' ((a *' (b + c)) ` ) = Bot L
by A8, Th27; verum