for L being 0_Lattice
for X, Y being Element of L holds
( X "\/" Y = Bottom L iff ( X = Bottom L & Y = Bottom L ) ) by LATTICES:5, LATTICES:16;