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