for L being B_Lattice
for X, Y, Z being Element of L holds
( X misses Y "\/" Z iff ( X misses Y & X misses Z ) ) by Th49;