let L be non trivial bounded Semilattice; :: thesis: for x being Element of L st x is dense holds
x <> Bottom L
let x be Element of L; :: thesis: ( x is dense implies x <> Bottom L )
assume A1: x is dense ; :: thesis: x <> Bottom L
Top L <> Bottom L by WAYBEL_7:3;
then x "/\" (Top L) <> Bottom L by A1;
hence x <> Bottom L by WAYBEL_1:4; :: thesis: verum