for L being non empty join-associative meet-commutative meet-absorbing join-absorbing orthomodular OrthoLattStr
for x, y being Element of L holds x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y by LATTICES:5, Def1;