:: deftheorem defines infimum-dense LATTICE6:def 14 :
for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L) );