theorem Th12: :: OPENLATT:12

for L being D_Lattice
for a being Element of L
for x being set holds
( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )