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