:: deftheorem GADL0 defines bottom LATTAD_1:def 14 :
for L being GAD_Lattice st L is with_zero holds
for b₂ being Element of L holds
( b₂ = bottom L iff for a being Element of L holds b₂ "/\" a = b₂ );