let L be Huntington de_Morgan preOrthoLattice; :: thesis: Bot L = Bottom L
reconsider C = Bot L as Element of L ;
A1: for a being Element of L holds
( C "/\" a = C & a "/\" C = C )
proof
let a be Element of L; :: thesis: ( C "/\" a = C & a "/\" C = C )
reconsider a9 = a as Element of L ;
thus C "/\" a = (Bot L) *' a9 by Def23
.= C by Def9 ; :: thesis: a "/\" C = C
hence a "/\" C = C ; :: thesis: verum
end;
then L is lower-bounded ;
hence Bot L = Bottom L by A1, LATTICES:def 16; :: thesis: verum