let L be AD_Lattice; :: thesis: for x, y being Element of L holds (x "/\" y) "\/" y = y
let x, y be Element of L; :: thesis: (x "/\" y) "\/" y = y
(x "/\" y) "\/" y = (x "/\" y) "\/" (y "/\" y) by IMeet
.= (x "\/" y) "/\" y by DefD
.= y by DefA1 ;
hence (x "/\" y) "\/" y = y ; :: thesis: verum