let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for a, b, c being Element of L holds a + (b *' c) = (a + b) *' (a + c)
let a, b, c be Element of L; :: thesis: a + (b *' c) = (a + b) *' (a + c)
thus a + (b *' c) = ((a ` ) *' ((((b ` ) + (c ` )) ` ) ` )) ` by Th18
.= ((a ` ) *' ((b ` ) + (c ` ))) ` by Th3
.= (((a ` ) *' (b ` )) + ((a ` ) *' (c ` ))) ` by Th31
.= (((((a ` ) *' (b ` )) ` ) *' (((a ` ) *' (c ` )) ` )) ` ) ` by Th18
.= (((a ` ) *' (b ` )) ` ) *' (((a ` ) *' (c ` )) ` ) by Th3
.= (a + b) *' (((a ` ) *' (c ` )) ` ) by Th18
.= (a + b) *' (a + c) by Th18 ; :: thesis: verum