for L being B_Lattice
for X, Y being Element of L st (X `) "\/" (Y `) = X "\/" Y & X misses X ` & Y misses Y ` holds
( X = Y ` & Y = X ` )