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