let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: Bot L = Bottom (CLatt L)
reconsider C = Bot L as Element of (CLatt L) by Def11;
for a being Element of (CLatt L) holds
( C "/\" a = C & a "/\" C = C )
proof
let a be Element of (CLatt L); :: thesis: ( C "/\" a = C & a "/\" C = C )
reconsider a9 = a as Element of L by Def11;
thus C "/\" a = (Bot L) *' a9 by Def11
.= C by Def9 ; :: thesis: a "/\" C = C
hence a "/\" C = C ; :: thesis: verum
end;
hence Bot L = Bottom (CLatt L) by LATTICES:def 16; :: thesis: verum