let L be non empty join-commutative join-associative Huntington ComplLattStr ; :: 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