let L be complete algebraic LATTICE; :: thesis: 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
let p be Element of L; :: thesis: ( p is completely-irreducible implies 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 )
set A = { 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) ) ) } ;
assume p is completely-irreducible ; :: thesis: 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
then consider q being Element of L such that
A1: p < q and
A2: for s being Element of L st p < s holds
q <= s and
uparrow p = {p} \/ (uparrow q) by Th20;
p <= q by A1, ORDERS_2:def 10;
then A3: compactbelow p c= compactbelow q by WAYBEL13:1;
compactbelow p <> compactbelow q

proof

assume compactbelow p = compactbelow q ; :: thesis: contradiction
then p = sup (compactbelow q) by WAYBEL_8:def 3
.= q by WAYBEL_8:def 3 ;
hence contradiction by A1; :: thesis: verum

end;

then not compactbelow q c= compactbelow p by A3, XBOOLE_0:def 10;
then consider k1 being set such that
A4: k1 in compactbelow q and
A5: not k1 in compactbelow p by TARSKI:def 3;
k1 in { y where y is Element of L : ( q >= y & y is compact ) } by A4, WAYBEL_8:def 2;
then consider k being Element of L such that
A6: k = k1 and
A7: q >= k and
A8: k is compact ;
A9: k in the carrier of (CompactSublatt L) by A8, WAYBEL_8:def 1;
p <= p ;
then A10: p in uparrow p by WAYBEL_0:18;
not k <= p by A5, A6, A8, WAYBEL_8:4;
then not p in uparrow k by WAYBEL_0:18;
then A11: p in the carrier of L \ (uparrow k) by XBOOLE_0:def 5;
for y being Element of L holds
( not y in the carrier of L \ (uparrow k) or not p < y )

proof

given y being Element of L such that A12: y in the carrier of L \ (uparrow k) and
A13: p < y ; :: thesis: contradiction
q <= y by A2, A13;
then k <= y by A7, ORDERS_2:26;
then y in uparrow k by WAYBEL_0:18;
hence contradiction by A12, XBOOLE_0:def 5; :: thesis: verum

end;

then p is_maximal_in the carrier of L \ (uparrow k) by A11, WAYBEL_4:56;
then A14: p in { 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) ) ) } by A9, A10;

now

let a be Element of L; :: thesis: ( a in { 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) ) ) } implies p <= a )
assume a in { 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) ) ) } ; :: thesis: p <= a
then consider a1 being Element of L such that
A15: a1 = a and
A16: a1 in uparrow p and
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & a1 is_maximal_in the carrier of L \ (uparrow k) ) ;
thus p <= a by A15, A16, WAYBEL_0:18; :: thesis: verum

end;

then A17: p is_<=_than { 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) ) ) } by LATTICE3:def 8;
for u being Element of L st u is_<=_than { 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) ) ) } holds
p >= u by A14, LATTICE3:def 8;
hence 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 by A17, YELLOW_0:33; :: thesis: verum