theorem :: YELLOW_5:15
for L being LATTICE
for a being Element of L holds
( a meets a iff a <> Bottom L ) by Th2;