theorem :: WAYBEL16:30

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
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )