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) ) ) } ;
p <= p ;
then A1: p in uparrow p by WAYBEL_0:18;

now :: thesis: for a being Element of L st 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) ) ) } holds
p <= a

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 ex a1 being Element of L st
( a1 = a & a1 in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & a1 is_maximal_in the carrier of L \ (uparrow k) ) ) ;
hence p <= a by WAYBEL_0:18; :: thesis: verum

end;

then A2: 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;
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
A3: p < q and
A4: for s being Element of L st p < s holds
q <= s and
uparrow p = {p} \/ (uparrow q) by Th20;
A5: 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 A3; :: thesis: verum

end;

p <= q by A3, ORDERS_2:def 6;
then compactbelow p c= compactbelow q by WAYBEL13:1;
then not compactbelow q c= compactbelow p by A5;
then consider k1 being object such that
A6: k1 in compactbelow q and
A7: not k1 in compactbelow p ;
k1 in { y where y is Element of L : ( q >= y & y is compact ) } by A6, WAYBEL_8:def 2;
then consider k being Element of L such that
A8: k = k1 and
A9: q >= k and
A10: k is compact ;
A11: 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 A4, A13;
then k <= y by A9, ORDERS_2:3;
then y in uparrow k by WAYBEL_0:18;
hence contradiction by A12, XBOOLE_0:def 5; :: thesis: verum

end;

not k <= p by A7, A8, A10, WAYBEL_8:4;
then not p in uparrow k by WAYBEL_0:18;
then p in the carrier of L \ (uparrow k) by XBOOLE_0:def 5;
then A14: p is_maximal_in the carrier of L \ (uparrow k) by A11, WAYBEL_4:55;
k in the carrier of (CompactSublatt L) by A10, WAYBEL_8:def 1;
then 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 A1, A14;
then 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 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 A2, YELLOW_0:33; :: thesis: verum