:: deftheorem defines ex_glb_of LATTAD_1:def 9 :
for L being GAD_Lattice
for a, b being Element of L holds
( ex_glb_of a,b iff ex c being Element of L st
( c [= a & c [= b & ( for x being Element of L st x [= a & x [= b holds
x [= c ) ) );