let L be distributive complete LATTICE; ( 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
; 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; ( 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
; 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;
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; ( 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}
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
uparrow k = V
then
k is compact
by WAYBEL_8:2;
hence
k in the carrier of (CompactSublatt L)
by WAYBEL_8:def 1; 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 )
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; verum