theorem Th23: :: LATTICE6:23

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