let L be 0_Lattice; :: thesis: for X being Element of L holds X misses Bottom L
let X be Element of L; :: thesis: X misses Bottom L
assume X meets Bottom L ; :: thesis: contradiction
then X "/\" (Bottom L) <> Bottom L by Def4;
hence contradiction by LATTICES:15; :: thesis: verum