let L be non empty join-commutative join-associative Huntington ComplLattStr ; :: thesis: 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; :: thesis: ((((((((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; :: thesis: verum