:: deftheorem DefGLB defines glb LATTAD_1:def 11 :
for L being GAD_Lattice
for a, b being Element of L st ex_glb_of a,b holds
for b₄ being Element of L holds
( b₄ = glb (a,b) iff ( b₄ [= a & b₄ [= b & ( for x being Element of L st x [= a & x [= b holds
x [= b₄ ) ) );