let L be AD_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
x "\/" (y "/\" x) = (x "/\" x) "\/" (y "/\" x) by IMeet
.= (x "\/" y) "/\" x by DefD
.= x by DefA2 ;
hence x "\/" (y "/\" x) = x ; :: thesis: verum