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
the carrier of L \ (downarrow p) is Open Filter of L )
assume L opp is meet-continuous ; :: thesis: for p being Element of L st p is completely-irreducible holds
the carrier of L \ (downarrow p) is Open Filter of L
then A1: L opp is satisfying_MC ;
let p be Element of L; :: thesis: ( p is completely-irreducible implies the carrier of L \ (downarrow p) is Open Filter of L )
assume A2: p is completely-irreducible ; :: thesis: the carrier of L \ (downarrow p) is Open Filter of L
not Top L in Irr L by Th21;
then A3: p <> Top L by A2, Def4;
p is meet-irreducible by A2, Th23;
then p is prime by WAYBEL_6:27;
then (downarrow p) ` is Filter of L by A3, WAYBEL_6:26;
then reconsider V = the carrier of L \ (downarrow p) as Filter of L by SUBSET_1:def 5;
consider q being Element of L such that
A4: p < q and
A5: for s being Element of L st p < s holds
q <= s and
uparrow p = {p} \/ (uparrow q) by A2, 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 A4, ORDERS_2:30;
then A6: q in F ;

now

let x, y be Element of L; :: thesis: ( x in F & y in F implies ex z being Element of the carrier of L st
( z in F & z <= x & z <= y ) )
assume that
A7: x in F and
A8: y in F ; :: thesis: ex z being Element of the carrier of L st
( z in F & z <= x & z <= y )
take z = x "/\" y; :: thesis: ( z in F & z <= x & z <= y )
consider x1 being Element of L such that
A9: x1 = x and
A10: x1 <= q and
A11: not x1 <= p by A7;
consider y1 being Element of L such that
A12: y1 = y and
A13: y1 <= q and
A14: not y1 <= p by A8;
A15: z <= x by YELLOW_0:23;
then A16: z <= q by A9, A10, ORDERS_2:26;
not z <= p

proof

assume A17: z <= p ; :: thesis: contradiction
A18: q >= p by A4, ORDERS_2:def 10;

A19: now

let d be Element of L; :: thesis: ( d >= y & d >= p implies q <= d )
assume that
A20: d >= y and
A21: d >= p ; :: thesis: q <= d
d > p by A12, A14, A20, A21, ORDERS_2:def 10;
hence q <= d by A5; :: thesis: verum

end;

x = x "/\" q by A9, A10, YELLOW_0:25
.= x "/\" (y "\/" p) by A12, A13, A18, A19, YELLOW_0:22
.= z "\/" (x "/\" p) by WAYBEL_1:def 3
.= (x "\/" z) "/\" (z "\/" p) by WAYBEL_1:6
.= x "/\" (p "\/" z) by A15, YELLOW_0:24
.= x "/\" p by A17, YELLOW_0:24 ;
hence contradiction by A9, A11, YELLOW_0:25; :: thesis: verum

end;

hence z in F by A16; :: thesis: ( z <= x & z <= y )
thus z <= x by YELLOW_0:23; :: thesis: z <= y
thus z <= y by YELLOW_0:23; :: thesis: verum

end;

then reconsider F = F as non empty filtered Subset of L by A6, WAYBEL_0:def 2;
reconsider F1 = F as non empty directed Subset of (L opp ) by YELLOW_7:27;

now

let x be Element of L; :: thesis: ( x in V implies ex y being Element of the carrier of L st
( y in V & y << x ) )
assume A22: x in V ; :: thesis: ex y being Element of the carrier of L st
( y in V & y << x )
take y = inf F; :: thesis: ( y in V & y << x )
thus y in V :: thesis: y << x

proof

ex_inf_of F,L by YELLOW_0:17;
then A23: inf F = sup F1 by YELLOW_7:13;
A24: ex_inf_of {(p ~ )} "/\" F1,L by YELLOW_0:17;
A25: {(p ~ )} = {p} by LATTICE3:def 6;
assume not y in V ; :: thesis: contradiction
then y in downarrow p by XBOOLE_0:def 5;
then y <= p by WAYBEL_0:17;
then A26: 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 A24, YELLOW_7:13
.= "/\" ({p} "\/" F),L by A25, Th5 ;

now

let r be Element of L; :: thesis: ( r in {p} "\/" F implies q <= r )
assume r in {p} "\/" F ; :: thesis: q <= r
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
A27: r = p "\/" v and
A28: v in F ;
A29: p <= r by A27, YELLOW_0:22;
consider v1 being Element of L such that
A30: v = v1 and
v1 <= q and
A31: not v1 <= p by A28;
p <> r by A27, A30, A31, YELLOW_0:24;
then p < r by A29, ORDERS_2:def 10;
hence q <= r by A5; :: thesis: verum

end;

then q is_<=_than {p} "\/" F by LATTICE3:def 8;
then q <= p by A26, YELLOW_0:33;
hence contradiction by A4, ORDERS_2:30; :: thesis: verum

end;

then not y in downarrow p by XBOOLE_0:def 5;
then A32: not y <= p by WAYBEL_0:17;
A33: x "/\" q <= x by YELLOW_0:23;
A34: y is_<=_than F by YELLOW_0:33;
A35: x "/\" q <= q by YELLOW_0:23;
not x in downarrow p by A22, XBOOLE_0:def 5;
then not x <= p by WAYBEL_0:17;
then not x "/\" q <= p by A4, A5, Th28;
then x "/\" q in F by A35;
then y <= x "/\" q by A34, LATTICE3:def 8;
then A36: y <= x by A33, ORDERS_2:26;

now

let D be non empty directed Subset of L; :: thesis: ( y <= sup D implies ex d being Element of L st
( d in D & y <= d ) )
assume A37: y <= sup D ; :: thesis: ex d being Element of L st
( d in D & y <= d )
not D \ (downarrow p) is empty

proof

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

end;

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

end;

then y << y by WAYBEL_3:def 1;
hence y << x by A36, WAYBEL_3:2; :: thesis: verum

end;

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