let L be GAD_Lattice; :: thesis: 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; :: thesis: ( 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) ) ) :: thesis: ( ex_glb_of x,y & x "/\" y = glb (x,y) implies x "/\" y = y "/\" x )

proof

assume x "/\" y = y "/\" x ; :: thesis: ( ex_glb_of x,y & x "/\" y = glb (x,y) )
then x "/\" y [= x by LATTICES:def 8;
hence ( ex_glb_of x,y & x "/\" y = glb (x,y) ) by ThXXX; :: thesis: verum

end;

assume ( ex_glb_of x,y & x "/\" y = glb (x,y) ) ; :: thesis: x "/\" y = y "/\" x
then x "/\" y [= x by DefGLB;
hence x "/\" y = y "/\" x by Th3715; :: thesis: verum