let L be GAD_Lattice; :: thesis: for x, y being Element of L st y "/\" x [= y holds
( ex_glb_of x,y & y "/\" x = glb (x,y) )
let x, y be Element of L; :: thesis: ( y "/\" x [= y implies ( ex_glb_of x,y & y "/\" x = glb (x,y) ) )
assume A1: y "/\" x [= y ; :: thesis: ( ex_glb_of x,y & y "/\" x = glb (x,y) )
A2: y "/\" x [= x 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 ) )

proof

take c = y "/\" x; :: thesis: ( c [= x & c [= y & ( for d being Element of L st d [= x & d [= y holds
d [= c ) )
thus ( c [= x & c [= y ) by A1, LATTICES:def 8; :: thesis: for d being Element of L st d [= x & d [= y holds
d [= c
let d be Element of L; :: thesis: ( d [= x & d [= y implies d [= c )
assume ( d [= x & d [= y ) ; :: thesis: d [= c
hence d [= c by DefLDS; :: thesis: verum

end;

hence T1: ex_glb_of x,y ; :: thesis: y "/\" x = glb (x,y)
for d being Element of L st d [= x & d [= y holds
d [= y "/\" x by DefLDS;
hence y "/\" x = glb (x,y) by T1, DefGLB, A1, A2; :: thesis: verum