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