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