let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: 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 Th9 ; :: thesis: verum