:: deftheorem DefLUB defines lub LATTAD_1:def 10 :
for L being GAD_Lattice
for a, b being Element of L st ex_lub_of a,b holds
for b₄ being Element of L holds
( b₄ = lub (a,b) iff ( a [= b₄ & b [= b₄ & ( for x being Element of L st a [= x & b [= x holds
b₄ [= x ) ) );