let L be GAD_Lattice; :: thesis: for x, y being Element of L holds
( x "/\" y = y "/\" x iff ( ex_glb_of x,y & y "/\" x = glb (x,y) ) )
let x, y be Element of L; :: thesis: ( x "/\" y = y "/\" x iff ( ex_glb_of x,y & y "/\" x = glb (x,y) ) )
thus ( x "/\" y = y "/\" x implies ( ex_glb_of x,y & y "/\" x = glb (x,y) ) ) :: thesis: ( ex_glb_of x,y & y "/\" x = glb (x,y) implies x "/\" y = y "/\" x )

proof

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

end;

assume ( ex_glb_of x,y & y "/\" x = glb (x,y) ) ; :: thesis: x "/\" y = y "/\" x
hence x "/\" y = y "/\" x by Th391i4, Th3965; :: thesis: verum