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