for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y & X [= Z & Y misses Z holds
X = Bottom L by Th9, FILTER_0:7;