:: deftheorem defines with_zero LATTAD_1:def 13 :
for L being GAD_Lattice holds
( L is with_zero iff ex x being Element of L st
for a being Element of L holds x "/\" a = x );