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)) ` ) = 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 Th27, Th28;
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 Th25 ;
hence ((a *' b) + (a *' c)) + ((a *' (b + c)) ` ) = Top L ; :: thesis: verum