let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ; :: thesis: for a being Element of L holds Bot L = (a + (a `)) `
let a be Element of L; :: thesis: Bot L = (a + (a `)) `
for b being Element of L holds ((a + (a `)) `) *' b = (a + (a `)) `

proof

let b be Element of L; :: thesis: ((a + (a `)) `) *' b = (a + (a `)) `
((a + (a `)) `) *' b = ((((b + (b `)) `) `) + (b `)) ` by Th4
.= ((b + (b `)) + (b `)) ` by Th3
.= (b + ((b `) + (b `))) ` by LATTICES:def 5
.= (b + (b `)) ` by Def7
.= ((a `) + a) ` by Th4 ;
hence ((a + (a `)) `) *' b = (a + (a `)) ` ; :: thesis: verum

end;

hence Bot L = (a + (a `)) ` by Def9; :: thesis: verum