for L being 0_Lattice
for X, Y, Z being Element of L st ( X misses Y or X misses Z ) holds
X misses Y "/\" Z by Th14;