theorem Th17: :: OPENLATT:17

for L being D_Lattice
for a, b being Element of L
for x being set st x in (SF_have b) \ (SF_have a) holds
( x is Filter of L & b in x & not a in x )