let L be GAD_Lattice; :: thesis: for x, y, z being Element of L holds (x "/\" y) "/\" z = (y "/\" x) "/\" z
let x, y, z be Element of L; :: thesis: (x "/\" y) "/\" z = (y "/\" x) "/\" z
A1: x "/\" z [= z by LATTICES:def 8;
y "/\" z [= z by LATTICES:def 8;
then (x "/\" z) "\/" (y "/\" z) = (y "/\" z) "\/" (x "/\" z) by DefB2, A1;
then (x "/\" z) "/\" (y "/\" z) = (y "/\" z) "/\" (x "/\" z) by IffComm;
then ((x "/\" z) "/\" y) "/\" z = (y "/\" z) "/\" (x "/\" z) by LATTICES:def 7;
then ((x "/\" z) "/\" y) "/\" z = ((y "/\" z) "/\" x) "/\" z by LATTICES:def 7;
then (x "/\" z) "/\" (y "/\" z) = ((y "/\" z) "/\" x) "/\" z by LATTICES:def 7;
then x "/\" (z "/\" (y "/\" z)) = ((y "/\" z) "/\" x) "/\" z by LATTICES:def 7;
then x "/\" (y "/\" z) = ((y "/\" z) "/\" x) "/\" z by Lem36c;
then (x "/\" y) "/\" z = ((y "/\" z) "/\" x) "/\" z by LATTICES:def 7;
then (x "/\" y) "/\" z = (y "/\" z) "/\" (x "/\" z) by LATTICES:def 7;
then (x "/\" y) "/\" z = y "/\" (z "/\" (x "/\" z)) by LATTICES:def 7;
then (x "/\" y) "/\" z = y "/\" (x "/\" z) by Lem36c;
hence (x "/\" y) "/\" z = (y "/\" x) "/\" z by LATTICES:def 7; :: thesis: verum