let L be GAD_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 v2, v0 being Element of L holds v2 "/\" (v0 "/\" v2) = v0 "/\" v2

proof

let v2, v0 be Element of L; :: thesis: v2 "/\" (v0 "/\" v2) = v0 "/\" v2
(v0 "/\" v2) "\/" v2 = v2 by LATTICES:def 8;
hence v2 "/\" (v0 "/\" v2) = v0 "/\" v2 by DefA2; :: thesis: verum

end;

hence x "/\" (y "/\" x) = y "/\" x ; :: thesis: verum