let L be GAD_Lattice; :: thesis: for x, y being Element of L holds x "\/" (x "\/" y) = x "\/" y
let x, y be Element of L; :: thesis: x "\/" (x "\/" y) = x "\/" y
x "/\" (x "\/" y) = x by LATTICES:def 9;
hence x "\/" (x "\/" y) = x "\/" y by LATTICES:def 8; :: thesis: verum