let L be 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) ) )
let x, y be Element of L; ( x "/\" y = y "/\" x iff ( ex_glb_of x,y & x "/\" y = glb (x,y) ) )
thus
( x "/\" y = y "/\" x implies ( ex_glb_of x,y & x "/\" y = glb (x,y) ) )
( ex_glb_of x,y & x "/\" y = glb (x,y) implies x "/\" y = y "/\" x )
assume
( ex_glb_of x,y & x "/\" y = glb (x,y) )
; x "/\" y = y "/\" x
then
x "/\" y [= x
by DefGLB;
hence
x "/\" y = y "/\" x
by Th3715; verum