let L be distributive complete LATTICE; :: thesis:
assume A1: L opp is meet-continuous ; :: thesis:
let p be Element of L; :: thesis:
assume A2: p is completely-irreducible ; :: thesis:
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;
defpred S₁[ Element of L] means ( $1 <= q & not $1 <= p );
reconsider F = { t where t is Element of L : S₁[t] } as Subset of L from DOMAIN_1:sch 7();
not q <= p by A3, ORDERS_2:6;
then A5: q in F ;

A6: now :: thesis:

let x, y be Element of L; :: thesis:
assume that
A7: x in F and
A8: y in F ; :: thesis:
A9: ex x1 being Element of L st
( x1 = x & x1 <= q & not x1 <= p ) by A7;
take z = x "/\" y; :: thesis:
A10: z <= x by YELLOW_0:23;
A11: ex y1 being Element of L st
( y1 = y & y1 <= q & not y1 <= p ) by A8;
A12: not z <= p

A13: now :: thesis:

let d be Element of L; :: thesis:
assume ( d >= y & d >= p ) ; :: thesis:
then d > p by A11, ORDERS_2:def 6;
hence q <= d by A4; :: thesis:

end;

assume A14: z <= p ; :: thesis:
A15: q >= p by A3, ORDERS_2:def 6;
x = x "/\" q by A9, YELLOW_0:25
.= x "/\" (y "\/" p) by A11, A15, A13, YELLOW_0:22
.= z "\/" (x "/\" p) by WAYBEL_1:def 3
.= (x "\/" z) "/\" (z "\/" p) by WAYBEL_1:5
.= x "/\" (p "\/" z) by A10, YELLOW_0:24
.= x "/\" p by A14, YELLOW_0:24 ;
hence contradiction by A9, YELLOW_0:25; :: thesis:

end;

z <= q by A9, A10, ORDERS_2:3;
hence z in F by A12; :: thesis:
thus z <= x by YELLOW_0:23; :: thesis:
thus z <= y by YELLOW_0:23; :: thesis:

end;

p is irreducible by A2, Th23;
then A16: p is prime by WAYBEL_6:27;
not Top L in Irr L by Th21;
then p <> Top L by A2, Def4;
then (downarrow p) ` is Filter of L by A16, WAYBEL_6:26;
then reconsider V = the carrier of L \ (downarrow p) as Filter of L by SUBSET_1:def 4;
reconsider F = F as non empty filtered Subset of L by A5, A6, WAYBEL_0:def 2;
reconsider F1 = F as non empty directed Subset of (L opp) by YELLOW_7:27;

let x be Element of L; :: thesis:
assume A17: x in V ; :: thesis:
take y = inf F; :: thesis:
thus y in V :: thesis:

let r be Element of L; :: thesis:
assume r in {p} "\/" F ; :: thesis:
then r in { (p "\/" v) where v is Element of L : v in F } by YELLOW_4:15;
then consider v being Element of L such that
A18: r = p "\/" v and
A19: v in F ;
ex v1 being Element of L st
( v = v1 & v1 <= q & not v1 <= p ) by A19;
then A20: p <> r by A18, YELLOW_0:24;
p <= r by A18, YELLOW_0:22;
then p < r by A20, ORDERS_2:def 6;
hence q <= r by A4; :: thesis:

end;

then A21: q is_<=_than {p} "\/" F by LATTICE3:def 8;
A22: ex_inf_of {(p ~)} "/\" F1,L by YELLOW_0:17;
ex_inf_of F,L by YELLOW_0:17;
then A23: inf F = sup F1 by YELLOW_7:13;
A24: {(p ~)} = {p} by LATTICE3:def 6;
assume not y in V ; :: thesis:
then y in downarrow p by XBOOLE_0:def 5;
then y <= p by WAYBEL_0:17;
then p = p "\/" y by YELLOW_0:24
.= (p ~) "/\" ((inf F) ~) by YELLOW_7:23
.= (p ~) "/\" (sup F1) by A23, LATTICE3:def 6
.= sup ({(p ~)} "/\" F1) by A1, WAYBEL_2:def 6
.= "/\" (({(p ~)} "/\" F1),L) by A22, YELLOW_7:13
.= "/\" (({p} "\/" F),L) by A24, Th5 ;
then q <= p by A21, YELLOW_0:33;
hence contradiction by A3, ORDERS_2:6; :: thesis:

end;

then not y in downarrow p by XBOOLE_0:def 5;
then A25: not y <= p by WAYBEL_0:17;

let D be non empty directed Subset of L; :: thesis:
assume A26: y <= sup D ; :: thesis:
not D \ (downarrow p) is empty

assume D \ (downarrow p) is empty ; :: thesis:
then D c= downarrow p by XBOOLE_1:37;
then sup D <= sup (downarrow p) by WAYBEL_7:1;
then y <= sup (downarrow p) by A26, ORDERS_2:3;
hence contradiction by A25, WAYBEL_0:34; :: thesis:

end;

then consider d being object such that
A27: d in D \ (downarrow p) ;
reconsider d = d as Element of L by A27;
take d = d; :: thesis:
thus d in D by A27, XBOOLE_0:def 5; :: thesis:
not d in downarrow p by A27, XBOOLE_0:def 5;
then not d <= p by WAYBEL_0:17;
then ( d "/\" q <= q & not d "/\" q <= p ) by A3, A4, Th28, YELLOW_0:23;
then ( y is_<=_than F & d "/\" q in F ) by YELLOW_0:33;
then ( d "/\" q <= d & y <= d "/\" q ) by LATTICE3:def 8, YELLOW_0:23;
hence y <= d by ORDERS_2:3; :: thesis:

end;

then A28: y << y by WAYBEL_3:def 1;
not x in downarrow p by A17, XBOOLE_0:def 5;
then not x <= p by WAYBEL_0:17;
then ( x "/\" q <= q & not x "/\" q <= p ) by A3, A4, Th28, YELLOW_0:23;
then ( y is_<=_than F & x "/\" q in F ) by YELLOW_0:33;
then ( x "/\" q <= x & y <= x "/\" q ) by LATTICE3:def 8, YELLOW_0:23;
then y <= x by ORDERS_2:3;
hence y << x by A28, WAYBEL_3:2; :: thesis:

end;

hence the carrier of L \ (downarrow p) is Open Filter of L by WAYBEL_6:def 1; :: thesis: