theorem Th24: :: LATTICE6:24

for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff for a being Element of L holds a = "/\" ( { d where d is Element of L : ( d in D & a [= d ) } ,L) )