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

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