for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y "/\" Z holds
( X meets Y & X meets Z )