theorem :: BOOLEALG:17

for L being 0_Lattice
for X, Y, Z being Element of L st X misses Z & Y [= Z holds
X misses Y by Th13;