for L being Lattice
for X being Element of L holds
( X meets X iff X <> Bottom L ) ;