let L be AD_Lattice; :: thesis: for x, y being Element of L holds x "/\" (y "/\" x) = y "/\" x
let x, y be Element of L; :: thesis: x "/\" (y "/\" x) = y "/\" x
for y, x being Element of L holds y "/\" (x "/\" y) = x "/\" y
proof
let y, x be Element of L; :: thesis: y "/\" (x "/\" y) = x "/\" y
(x "/\" y) "\/" y = y by LemXX;
hence y "/\" (x "/\" y) = x "/\" y by DefA2; :: thesis: verum
end;
hence x "/\" (y "/\" x) = y "/\" x ; :: thesis: verum