thus CLatt L is lower-bounded :: thesis: verum
proof
set c9 = Bot L;
reconsider c = Bot L as Element of (CLatt L) by Def11;
take c ; :: according to LATTICES:def 13 :: thesis: for b1 being M3( the carrier of (CLatt L)) holds
( c "/\" b1 = c & b1 "/\" c = c )
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;