theorem Th29: :: WAYBEL16:29

for L being distributive complete LATTICE st L opp is meet-continuous holds
for p being Element of L st p is completely-irreducible holds
the carrier of L \ (downarrow p) is Open Filter of L