let L be non empty join-commutative join-associative Huntington ComplLLattStr ; 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 ` ))
let a, b, c be Element of L; (a *' (b + c)) ` = (((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' 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 ` );
A1: a ` =
((a ` ) *' b) + ((a ` ) *' (b ` ))
by Def6
.=
((((a ` ) *' b) *' c) + (((a ` ) *' b) *' (c ` ))) + ((a ` ) *' (b ` ))
by Def6
.=
((((a ` ) *' b) *' c) + (((a ` ) *' b) *' (c ` ))) + ((((a ` ) *' (b ` )) *' c) + (((a ` ) *' (b ` )) *' (c ` )))
by Def6
;
A2: (b ` ) *' (c ` ) =
(a *' ((b ` ) *' (c ` ))) + ((a ` ) *' ((b ` ) *' (c ` )))
by Th1
.=
((a *' (b ` )) *' (c ` )) + ((a ` ) *' ((b ` ) *' (c ` )))
by Th17
.=
((a *' (b ` )) *' (c ` )) + (((a ` ) *' (b ` )) *' (c ` ))
by Th17
;
(a *' (b + c)) ` =
(a ` ) + ((b + c) ` )
by Th3
.=
(a ` ) + ((((b ` ) *' (c ` )) ` ) ` )
by Th18
.=
(a ` ) + ((b ` ) *' (c ` ))
by Th3
;
hence (a *' (b + c)) ` =
((((((a ` ) *' b) *' c) + (((a ` ) *' b) *' (c ` ))) + ((((a ` ) *' (b ` )) *' c) + (((a ` ) *' (b ` )) *' (c ` )))) + (((a ` ) *' (b ` )) *' (c ` ))) + ((a *' (b ` )) *' (c ` ))
by A1, A2, LATTICES:def 5
.=
(((((((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 ` ))
by LATTICES:def 5
.=
((((((a ` ) *' b) *' c) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` ))) + ((a *' (b ` )) *' (c ` ))
by Def7
.=
((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 ` )))
by LATTICES:def 5
.=
((((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 ` ))
by LATTICES:def 5
;
verum