:: deftheorem defines SF_have OPENLATT:def 8 :
for L being D_Lattice
for a being Element of L holds SF_have a = { F where F is Filter of L : a in F } ;