for L being distributive bounded well-complemented preOrthoLattice
for x, y being Element of L holds x "/\" y = ((x `) "\/" (y `)) `