for L being GAD_Lattice
for x, y being Element of L holds
( x "/\" y = y "/\" x iff ( ex_glb_of x,y & x "/\" y = glb (x,y) ) )