for L being complete algebraic LATTICE
for p being Element of L st p is completely-irreducible holds
p = "/\" ( { x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } ,L)