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 Th17
.= ((a `) *' ((b `) + (c `))) ` by Th3
.= (((a `) *' (b `)) + ((a `) *' (c `))) ` by Th30
.= (((((a `) *' (b `)) `) *' (((a `) *' (c `)) `)) `) ` by Th17
.= (((a `) *' (b `)) `) *' (((a `) *' (c `)) `) by Th3
.= (a + b) *' (((a `) *' (c `)) `) by Th17
.= (a + b) *' (a + c) by Th17 ; :: thesis: verum