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