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: I in { P where P is Ideal of L : ( I c= P & P misses F ) } by A1;

A3: now

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;

now

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 <> {} & Z c= { P where P is Ideal of L : ( I c= P & P misses F ) } ) and
A5: 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 set ; :: 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 A4;
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

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 A4;
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;

A6: now

consider x being Element of I, y being Element of Z;
( y in Z & x in I ) by A4;
then ( I c= y & y c= J ) by A3, A4, ZFMISC_1:92;
hence I c= J by XBOOLE_1:1; :: 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 ) ) )
hence not J is empty ; :: 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 A8: ( 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 A5, ORDINAL1:def 9;
then ( A c= B or B c= A ) by XBOOLE_0:def 9;
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 A8; :: thesis: verum

end;

now

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 A4;
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 A6, WAYBEL_0:46;

now

let x be set ; :: 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
A9: ( x in A & A in Z ) by TARSKI:def 4;
A misses F by A3, A4, A9;
hence not x in F by A9, 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 A6; :: thesis: verum

end;

then consider Y being set such that
A10: ( Y in { P where P is Ideal of L : ( I c= P & P misses F ) } & ( 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 A2, ORDERS_1:177;
consider P being Ideal of L such that
A11: ( P = Y & I c= P & P misses F ) by A10;
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 A12: ( x "/\" y in P & not x in P & not y in P ) ; :: thesis: contradiction
set Px = downarrow (finsups (P \/ {x}));
set Py = downarrow (finsups (P \/ {y}));
( x in {x} & y in {y} ) by TARSKI:def 1;
then ( x in P \/ {x} & P \/ {x} c= downarrow (finsups (P \/ {x})) & y in P \/ {y} & P \/ {y} c= downarrow (finsups (P \/ {y})) & P c= P \/ {x} & P c= P \/ {y} ) by WAYBEL_0:61, XBOOLE_0:def 3, XBOOLE_1:7;
then A13: ( x in downarrow (finsups (P \/ {x})) & P c= downarrow (finsups (P \/ {x})) & y in downarrow (finsups (P \/ {y})) & P c= downarrow (finsups (P \/ {y})) ) by XBOOLE_1:1;
then A14: ( I c= downarrow (finsups (P \/ {x})) & I c= downarrow (finsups (P \/ {y})) & downarrow (finsups (P \/ {x})) is Ideal of L & downarrow (finsups (P \/ {y})) is Ideal of L ) by A11, XBOOLE_1:1;

now

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 A14;
hence contradiction by A10, A11, A12, A13; :: thesis: verum

end;

then consider u being set such that
A15: ( u in downarrow (finsups (P \/ {x})) & u in F ) by XBOOLE_0:3;

now

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 A14;
hence contradiction by A10, A11, A12, A13; :: thesis: verum

end;

then consider v being set such that
A16: ( v in downarrow (finsups (P \/ {y})) & v in F ) by XBOOLE_0:3;
reconsider u = u, v = v as Element of L by A15, A16;
consider u' being Element of L such that
A17: ( u' in P & u <= u' "\/" (sup {x}) ) by A15, Lm2;
consider v' being Element of L such that
A18: ( v' in P & v <= v' "\/" (sup {y}) ) by A16, Lm2;
A19: ( sup {x} = x & sup {y} = y ) by YELLOW_0:39;
set w = u' "\/" v';
A20: u' "\/" v' in P by A17, A18, WAYBEL_0:40;
( (u' "\/" v') "\/" y = u' "\/" (v' "\/" y) & (v' "\/" u') "\/" x = v' "\/" (u' "\/" x) & v' "\/" u' = u' "\/" v' ) by LATTICE3:14;
then ( (u' "\/" v') "\/" y >= v' "\/" y & (u' "\/" v') "\/" x >= u' "\/" x ) by YELLOW_0:22;
then ( (u' "\/" v') "\/" x >= u & (u' "\/" v') "\/" y >= v ) by A17, A18, A19, ORDERS_2:26;
then ( (u' "\/" v') "\/" x in F & (u' "\/" v') "\/" y in F ) by A15, A16, WAYBEL_0:def 20;
then ((u' "\/" v') "\/" x) "/\" ((u' "\/" v') "\/" y) in F by WAYBEL_0:41;
then ( (u' "\/" v') "\/" (x "/\" y) in F & (u' "\/" v') "\/" (x "/\" y) in P ) by A12, A20, WAYBEL_0:40, WAYBEL_1:6;
hence contradiction by A11, XBOOLE_0:3; :: thesis: verum

end;

thus ( I c= P & P misses F ) by A11; :: thesis: verum