theorem :: BOOLEALG:10

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