for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y & Y [= Z holds
X meets Z by Th9, LATTICES:9;