let L be non empty join-commutative join-associative Huntington ComplLattStr ; :: thesis: for a being Element of L holds a *' (a ` ) = Bot L
let a be Element of L; :: thesis: a *' (a ` ) = Bot L
thus a *' (a ` ) = (Top L) ` by Def8
.= Bot L by Th10 ; :: thesis: verum