let L be distributive complete LATTICE; :: thesis: ( L opp is meet-continuous implies 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) ) )
assume A1: L opp is meet-continuous ; :: thesis: 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) )
let p be Element of L; :: thesis: ( p is completely-irreducible implies ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) )
assume A2: p is completely-irreducible ; :: thesis: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
then reconsider V = the carrier of L \ (downarrow p) as Open Filter of L by A1, Th29;

now :: thesis: for b being Element of L st b in (uparrow p) \ {p} holds
p <= b

let b be Element of L; :: thesis: ( b in (uparrow p) \ {p} implies p <= b )
assume b in (uparrow p) \ {p} ; :: thesis: p <= b
then b in uparrow p by XBOOLE_0:def 5;
hence p <= b by WAYBEL_0:18; :: thesis: verum

end;

then p is_<=_than (uparrow p) \ {p} by LATTICE3:def 8;
then A3: p <= "/\" (((uparrow p) \ {p}),L) by YELLOW_0:33;
"/\" (((uparrow p) \ {p}),L) <> p by A2, Th19;
then A4: p < "/\" (((uparrow p) \ {p}),L) by A3, ORDERS_2:def 6;
A5: ( ex_inf_of V,L & (inf V) ~ = inf V ) by LATTICE3:def 6, YELLOW_0:17;
take k = inf V; :: thesis: ( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
reconsider V9 = V as non empty directed Subset of (L opp) by YELLOW_7:27;
A6: ex_inf_of {(p ~)} "/\" V9,L by YELLOW_0:17;
A7: ( ex_inf_of {p} "\/" V,L & ex_inf_of (uparrow p) \ {p},L ) by YELLOW_0:17;
A8: {p} "\/" V c= (uparrow p) \ {p}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {p} "\/" V or x in (uparrow p) \ {p} )
assume x in {p} "\/" V ; :: thesis: x in (uparrow p) \ {p}
then x in { (p "\/" v) where v is Element of L : v in V } by YELLOW_4:15;
then consider v being Element of L such that
A9: x = p "\/" v and
A10: v in V ;
not v in downarrow p by A10, XBOOLE_0:def 5;
then not v <= p by WAYBEL_0:17;
then p "\/" v <> p by YELLOW_0:22;
then A11: not p "\/" v in {p} by TARSKI:def 1;
p <= p "\/" v by YELLOW_0:22;
then p "\/" v in uparrow p by WAYBEL_0:18;
hence x in (uparrow p) \ {p} by A9, A11, XBOOLE_0:def 5; :: thesis: verum

end;

A12: p = p ~ by LATTICE3:def 6;
p "\/" k = (p ~) "/\" ((inf V) ~) by YELLOW_7:23
.= (p ~) "/\" ("\/" (V,(L opp))) by A5, YELLOW_7:13
.= "\/" (({(p ~)} "/\" V9),(L opp)) by A1, WAYBEL_2:def 6
.= "/\" (({(p ~)} "/\" V9),L) by A6, YELLOW_7:13
.= inf ({p} "\/" V) by A12, Th5 ;
then A13: "/\" (((uparrow p) \ {p}),L) <= p "\/" k by A7, A8, YELLOW_0:35;
A14: not k <= p

proof

assume k <= p ; :: thesis: contradiction
then p "\/" k = p by YELLOW_0:24;
hence contradiction by A13, A4, ORDERS_2:7; :: thesis: verum

end;

uparrow k = V

proof

thus uparrow k c= V :: according to XBOOLE_0:def 10 :: thesis: V c= uparrow k

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow k or x in V )
assume A15: x in uparrow k ; :: thesis: x in V
then reconsider x1 = x as Element of L ;
k <= x1 by A15, WAYBEL_0:18;
then not x1 <= p by A14, ORDERS_2:3;
then not x1 in downarrow p by WAYBEL_0:17;
hence x in V by XBOOLE_0:def 5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V or x in uparrow k )
assume A16: x in V ; :: thesis: x in uparrow k
then reconsider x1 = x as Element of L ;
k is_<=_than V by YELLOW_0:33;
then k <= x1 by A16, LATTICE3:def 8;
hence x in uparrow k by WAYBEL_0:18; :: thesis: verum

end;

then k is compact by WAYBEL_8:2;
hence k in the carrier of (CompactSublatt L) by WAYBEL_8:def 1; :: thesis: p is_maximal_in the carrier of L \ (uparrow k)
A17: 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 A18: y in the carrier of L \ (uparrow k) and
A19: p < y ; :: thesis: contradiction
not y in uparrow k by A18, XBOOLE_0:def 5;
then ( k is_<=_than V & not k <= y ) by WAYBEL_0:18, YELLOW_0:33;
then not y in V by LATTICE3:def 8;
then y in downarrow p by XBOOLE_0:def 5;
then y <= p by WAYBEL_0:17;
hence contradiction by A19, ORDERS_2:6; :: thesis: verum

end;

not p in uparrow k by A14, WAYBEL_0:18;
then p in the carrier of L \ (uparrow k) by XBOOLE_0:def 5;
hence p is_maximal_in the carrier of L \ (uparrow k) by A17, WAYBEL_4:55; :: thesis: verum