let L be GAD_Lattice; for x, y being Element of L st x "/\" y [= x holds
( ex_glb_of x,y & x "/\" y = glb (x,y) )
let x, y be Element of L; ( x "/\" y [= x implies ( ex_glb_of x,y & x "/\" y = glb (x,y) ) )
assume A1:
x "/\" y [= x
; ( ex_glb_of x,y & x "/\" y = glb (x,y) )
A2:
x "/\" y [= y
by LATTICES:def 8;
ex c being Element of L st
( c [= x & c [= y & ( for d being Element of L st d [= x & d [= y holds
d [= c ) )
hence T1:
ex_glb_of x,y
; x "/\" y = glb (x,y)
for d being Element of L st d [= x & d [= y holds
d [= x "/\" y
by DefLDS;
hence
x "/\" y = glb (x,y)
by T1, DefGLB, A1, A2; verum