:: deftheorem defines % LATTICE6:def 2 :
for L being Lattice
for D being Subset of (LattPOSet L) holds % D = { (% d) where d is Element of (LattPOSet L) : d in D } ;