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