for L being complete algebraic LATTICE
for p being Element of L 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) ) iff p is completely-irreducible )