let L be distributive LATTICE; :: thesis: for I being Ideal of L
for F being Filter of L st I misses F holds
ex P being Ideal of L st
( P is prime & I c= P & P misses F )
let I be Ideal of L; :: thesis: for F being Filter of L st I misses F holds
ex P being Ideal of L st
( P is prime & I c= P & P misses F )
let F be Filter of L; :: thesis: ( I misses F implies ex P being Ideal of L st
( P is prime & I c= P & P misses F ) )
assume A1: I misses F ; :: thesis: ex P being Ideal of L st
( P is prime & I c= P & P misses F )
set X = { P where P is Ideal of L : ( I c= P & P misses F ) } ;

A2: now :: thesis: for A being set st A in { P where P is Ideal of L : ( I c= P & P misses F ) } holds
( I c= A & A misses F )

let A be set ; :: thesis: ( A in { P where P is Ideal of L : ( I c= P & P misses F ) } implies ( I c= A & A misses F ) )
assume A in { P where P is Ideal of L : ( I c= P & P misses F ) } ; :: thesis: ( I c= A & A misses F )
then ex P being Ideal of L st
( A = P & I c= P & P misses F ) ;
hence ( I c= A & A misses F ) ; :: thesis: verum

end;

A3: now :: thesis: for Z being set st Z <> {} & Z c= { P where P is Ideal of L : ( I c= P & P misses F ) } & Z is c=-linear holds
union Z in { P where P is Ideal of L : ( I c= P & P misses F ) }

let Z be set ; :: thesis: ( Z <> {} & Z c= { P where P is Ideal of L : ( I c= P & P misses F ) } & Z is c=-linear implies union Z in { P where P is Ideal of L : ( I c= P & P misses F ) } )
assume that
A4: Z <> {} and
A5: Z c= { P where P is Ideal of L : ( I c= P & P misses F ) } and
A6: Z is c=-linear ; :: thesis: union Z in { P where P is Ideal of L : ( I c= P & P misses F ) }
Z c= bool the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in bool the carrier of L )
assume x in Z ; :: thesis: x in bool the carrier of L
then x in { P where P is Ideal of L : ( I c= P & P misses F ) } by A5;
then ex P being Ideal of L st
( x = P & I c= P & P misses F ) ;
hence x in bool the carrier of L ; :: thesis: verum

end;

then reconsider ZI = Z as Subset-Family of L ;

now :: thesis: for A being Subset of L st A in ZI holds
A is lower

let A be Subset of L; :: thesis: ( A in ZI implies A is lower )
assume A in ZI ; :: thesis: A is lower
then A in { P where P is Ideal of L : ( I c= P & P misses F ) } by A5;
then ex P being Ideal of L st
( A = P & I c= P & P misses F ) ;
hence A is lower ; :: thesis: verum

end;

then reconsider J = union ZI as lower Subset of L by WAYBEL_0:26;

A7: now :: thesis: ( I c= J & not J is empty & ( for A, B being Subset of L st A in ZI & B in ZI holds
ex C being Subset of L st
( C in ZI & A \/ B c= C ) ) )

set y = the Element of Z;
the Element of Z in Z by A4;
then A8: I c= the Element of Z by A2, A5;
A9: the Element of Z c= J by A4, ZFMISC_1:74;
hence I c= J by A8; :: thesis: ( not J is empty & ( for A, B being Subset of L st A in ZI & B in ZI holds
ex C being Subset of L st
( C in ZI & A \/ B c= C ) ) )
thus not J is empty by A8, A9; :: thesis: for A, B being Subset of L st A in ZI & B in ZI holds
ex C being Subset of L st
( C in ZI & A \/ B c= C )
let A, B be Subset of L; :: thesis: ( A in ZI & B in ZI implies ex C being Subset of L st
( C in ZI & A \/ B c= C ) )
assume A10: ( A in ZI & B in ZI ) ; :: thesis: ex C being Subset of L st
( C in ZI & A \/ B c= C )
then A,B are_c=-comparable by A6, ORDINAL1:def 8;
then ( A c= B or B c= A ) ;
then ( A \/ B = A or A \/ B = B ) by XBOOLE_1:12;
hence ex C being Subset of L st
( C in ZI & A \/ B c= C ) by A10; :: thesis: verum

end;

now :: thesis: for A being Subset of L st A in ZI holds
A is directed

let A be Subset of L; :: thesis: ( A in ZI implies A is directed )
assume A in ZI ; :: thesis: A is directed
then A in { P where P is Ideal of L : ( I c= P & P misses F ) } by A5;
then ex P being Ideal of L st
( A = P & I c= P & P misses F ) ;
hence A is directed ; :: thesis: verum

end;

then reconsider J = J as Ideal of L by A7, WAYBEL_0:46;

now :: thesis: for x being object st x in J holds
not x in F

let x be object ; :: thesis: ( x in J implies not x in F )
assume x in J ; :: thesis: not x in F
then consider A being set such that
A11: x in A and
A12: A in Z by TARSKI:def 4;
A misses F by A2, A5, A12;
hence not x in F by A11, XBOOLE_0:3; :: thesis: verum

end;

then J misses F by XBOOLE_0:3;
hence union Z in { P where P is Ideal of L : ( I c= P & P misses F ) } by A7; :: thesis: verum

end;

I in { P where P is Ideal of L : ( I c= P & P misses F ) } by A1;
then consider Y being set such that
A13: Y in { P where P is Ideal of L : ( I c= P & P misses F ) } and
A14: for Z being set st Z in { P where P is Ideal of L : ( I c= P & P misses F ) } & Z <> Y holds
not Y c= Z by A3, ORDERS_1:67;
consider P being Ideal of L such that
A15: P = Y and
A16: I c= P and
A17: P misses F by A13;
take P ; :: thesis: ( P is prime & I c= P & P misses F )

hereby :: according to WAYBEL_7:def 1 :: thesis: ( I c= P & P misses F )

let x, y be Element of L; :: thesis: ( x "/\" y in P & not x in P implies y in P )
assume that
A18: x "/\" y in P and
A19: not x in P and
A20: not y in P ; :: thesis: contradiction
set Py = downarrow (finsups (P \/ {y}));
A21: P \/ {y} c= downarrow (finsups (P \/ {y})) by WAYBEL_0:61;
A22: P c= P \/ {y} by XBOOLE_1:7;
then P c= downarrow (finsups (P \/ {y})) by A21;
then A23: I c= downarrow (finsups (P \/ {y})) by A16;
y in {y} by TARSKI:def 1;
then y in P \/ {y} by XBOOLE_0:def 3;
then A24: y in downarrow (finsups (P \/ {y})) by A21;

now :: thesis: not downarrow (finsups (P \/ {y})) misses F

assume downarrow (finsups (P \/ {y})) misses F ; :: thesis: contradiction
then downarrow (finsups (P \/ {y})) in { P where P is Ideal of L : ( I c= P & P misses F ) } by A23;
hence contradiction by A14, A15, A20, A21, A22, A24, XBOOLE_1:1; :: thesis: verum

end;

then consider v being object such that
A25: v in downarrow (finsups (P \/ {y})) and
A26: v in F by XBOOLE_0:3;
set Px = downarrow (finsups (P \/ {x}));
A27: P \/ {x} c= downarrow (finsups (P \/ {x})) by WAYBEL_0:61;
A28: P c= P \/ {x} by XBOOLE_1:7;
then P c= downarrow (finsups (P \/ {x})) by A27;
then A29: I c= downarrow (finsups (P \/ {x})) by A16;
x in {x} by TARSKI:def 1;
then x in P \/ {x} by XBOOLE_0:def 3;
then A30: x in downarrow (finsups (P \/ {x})) by A27;

now :: thesis: not downarrow (finsups (P \/ {x})) misses F

assume downarrow (finsups (P \/ {x})) misses F ; :: thesis: contradiction
then downarrow (finsups (P \/ {x})) in { P where P is Ideal of L : ( I c= P & P misses F ) } by A29;
hence contradiction by A14, A15, A19, A27, A28, A30, XBOOLE_1:1; :: thesis: verum

end;

then consider u being object such that
A31: u in downarrow (finsups (P \/ {x})) and
A32: u in F by XBOOLE_0:3;
reconsider u = u, v = v as Element of L by A31, A25;
consider u9 being Element of L such that
A33: u9 in P and
A34: u <= u9 "\/" (sup {x}) by A31, Lm2;
consider v9 being Element of L such that
A35: v9 in P and
A36: v <= v9 "\/" (sup {y}) by A25, Lm2;
set w = u9 "\/" v9;
(v9 "\/" u9) "\/" x = v9 "\/" (u9 "\/" x) by LATTICE3:14;
then ( sup {x} = x & (u9 "\/" v9) "\/" x >= u9 "\/" x ) by YELLOW_0:22, YELLOW_0:39;
then (u9 "\/" v9) "\/" x >= u by A34, ORDERS_2:3;
then A37: (u9 "\/" v9) "\/" x in F by A32, WAYBEL_0:def 20;
(u9 "\/" v9) "\/" y = u9 "\/" (v9 "\/" y) by LATTICE3:14;
then ( sup {y} = y & (u9 "\/" v9) "\/" y >= v9 "\/" y ) by YELLOW_0:22, YELLOW_0:39;
then (u9 "\/" v9) "\/" y >= v by A36, ORDERS_2:3;
then (u9 "\/" v9) "\/" y in F by A26, WAYBEL_0:def 20;
then ((u9 "\/" v9) "\/" x) "/\" ((u9 "\/" v9) "\/" y) in F by A37, WAYBEL_0:41;
then A38: (u9 "\/" v9) "\/" (x "/\" y) in F by WAYBEL_1:5;
u9 "\/" v9 in P by A33, A35, WAYBEL_0:40;
then (u9 "\/" v9) "\/" (x "/\" y) in P by A18, WAYBEL_0:40;
hence contradiction by A17, A38, XBOOLE_0:3; :: thesis: verum

end;

thus ( I c= P & P misses F ) by A16, A17; :: thesis: verum