let L be non empty join-commutative join-associative Huntington ComplLattStr ; :: 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 Th10
.= (a ` ) ` by Th14
.= a by Th3 ;
hence a *' (Top L) = a ; :: thesis: verum