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