for L being GAD_Lattice st ( for a, b being Element of L holds (a "\/" b) "/\" b = b ) holds
for a, b, c being Element of L holds (a "\/" b) "/\" c = (b "\/" a) "/\" c