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;
reconsider V' = V as non empty directed Subset of (L opp ) by YELLOW_7:27;
take k = inf V; :: thesis: ( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
A3: L opp is satisfying_MC by A1;
A4: ( ex_inf_of V,L & ex_inf_of {(p ~ )} "/\" V',L ) by YELLOW_0:17;
A5: ( ex_inf_of {p} "\/" V,L & ex_inf_of (uparrow p) \ {p},L ) by YELLOW_0:17;
A6: (inf V) ~ = inf V by LATTICE3:def 6;
A7: p = p ~ by LATTICE3:def 6;
A8: {p} "\/" V c= (uparrow p) \ {p}

proof

let x be set ; :: 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 <= p "\/" v & p "\/" v <> p ) by YELLOW_0:22;
then ( p "\/" v in uparrow p & not p "\/" v in {p} ) by TARSKI:def 1, WAYBEL_0:18;
hence x in (uparrow p) \ {p} by A9, XBOOLE_0:def 5; :: thesis: verum

end;

p "\/" k = (p ~ ) "/\" ((inf V) ~ ) by YELLOW_7:23
.= (p ~ ) "/\" ("\/" V,(L opp )) by A4, A6, YELLOW_7:13
.= "\/" ({(p ~ )} "/\" V'),(L opp ) by A3, WAYBEL_2:def 6
.= "/\" ({(p ~ )} "/\" V'),L by A4, YELLOW_7:13
.= inf ({p} "\/" V) by A7, Th5 ;
then A11: "/\" ((uparrow p) \ {p}),L <= p "\/" k by A5, A8, YELLOW_0:35;
A12: "/\" ((uparrow p) \ {p}),L <> p by A2, Th19;

now

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 p <= "/\" ((uparrow p) \ {p}),L by YELLOW_0:33;
then A13: p < "/\" ((uparrow p) \ {p}),L by A12, ORDERS_2:def 10;
A14: not k <= p

proof

assume k <= p ; :: thesis: contradiction
then p "\/" k = p by YELLOW_0:24;
hence contradiction by A11, A13, ORDERS_2:32; :: 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 set ; :: 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:26;
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 set ; :: 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)
not p in uparrow k by A14, WAYBEL_0:18;
then A17: 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 A18: y in the carrier of L \ (uparrow k) and
A19: p < y ; :: thesis: contradiction
A20: k is_<=_than V by YELLOW_0:33;
not y in uparrow k by A18, XBOOLE_0:def 5;
then not k <= y by WAYBEL_0:18;
then not y in V by A20, 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:30; :: thesis: verum

end;

hence p is_maximal_in the carrier of L \ (uparrow k) by A17, WAYBEL_4:56; :: thesis: verum