let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for a being Element of L holds a *' (Top L) = a
let a be Element of L; :: thesis: a *' (Top L) = a
a *' (Top L) = ((a `) + (Bot L)) ` by Th9
.= (a `) ` by Th13
.= a by Th3 ;
hence a *' (Top L) = a ; :: thesis: verum