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 = { i where i is Ideal of L : ( I c= i & i misses F ) } ;
z1: I in { i where i is Ideal of L : ( I c= i & i misses F ) } by A1;
for Z being set st Z <> {} & Z c= { i where i is Ideal of L : ( I c= i & i misses F ) } & Z is c=-linear holds
union Z in { i where i is Ideal of L : ( I c= i & i misses F ) }

proof

let Z be set ; :: thesis: ( Z <> {} & Z c= { i where i is Ideal of L : ( I c= i & i misses F ) } & Z is c=-linear implies union Z in { i where i is Ideal of L : ( I c= i & i misses F ) } )
assume s1: ( Z <> {} & Z c= { i where i is Ideal of L : ( I c= i & i misses F ) } & Z is c=-linear ) ; :: thesis: union Z in { i where i is Ideal of L : ( I c= i & i misses F ) }
BB: for x being object st x in Z holds
x is Ideal of L

proof

let x be object ; :: thesis: ( x in Z implies x is Ideal of L )
assume x in Z ; :: thesis: x is Ideal of L
then x in { i where i is Ideal of L : ( I c= i & i misses F ) } by s1;
then consider i being Ideal of L such that
SO: ( i = x & I c= i & i misses F ) ;
thus x is Ideal of L by SO; :: thesis: verum

end;

set M = union Z;
consider f being object such that
K1: f in Z by s1, XBOOLE_0:def 1;
reconsider f = f as set by TARSKI:1;
UU: union Z c= the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union Z or x in the carrier of L )
assume x in union Z ; :: thesis: x in the carrier of L
then consider g being set such that
U1: ( x in g & g in Z ) by TARSKI:def 4;
g is Ideal of L by U1, BB;
hence x in the carrier of L by U1; :: thesis: verum

end;

f in { i where i is Ideal of L : ( I c= i & i misses F ) } by K1, s1;
then consider j being Ideal of L such that
SF: ( f = j & I c= j & j misses F ) ;
f c= union Z by K1, ZFMISC_1:74;
then reconsider M = union Z as non empty Subset of L by SF, UU;

H0: now :: thesis: for a, b being Element of L st a in M & b in M holds
a "\/" b in M

let a, b be Element of L; :: thesis: ( a in M & b in M implies b₁ "\/" b₂ in M )
assume S1: ( a in M & b in M ) ; :: thesis: b₁ "\/" b₂ in M
then consider W being set such that
S2: ( a in W & W in Z ) by TARSKI:def 4;
consider V being set such that
S3: ( b in V & V in Z ) by S1, TARSKI:def 4;
H1: V is Ideal of L by S3, BB;
h1: W is Ideal of L by S2, BB;
W,V are_c=-comparable by s1, S2, S3, ORDINAL1:def 8;

per cases then ( W c= V or V c= W ) ;

suppose W c= V ; :: thesis: b₁ "\/" b₂ in M

then H2: a "\/" b in V by FILTER_2:21, H1, S2, S3;
V c= M by ZFMISC_1:74, S3;
hence a "\/" b in M by H2; :: thesis: verum

end;

suppose V c= W ; :: thesis: b₁ "\/" b₂ in M

then H2: a "\/" b in W by FILTER_2:21, h1, S2, S3;
W c= M by ZFMISC_1:74, S2;
hence a "\/" b in M by H2; :: thesis: verum

end;

end;

end;

for p, q being Element of L st p in M & q [= p holds
q in M

proof

let p, q be Element of L; :: thesis: ( p in M & q [= p implies q in M )
assume J0: ( p in M & q [= p ) ; :: thesis: q in M
then consider W being set such that
J1: ( p in W & W in Z ) by TARSKI:def 4;
W is Ideal of L by J1, BB;
then q in W by FILTER_2:21, J0, J1;
hence q in M by TARSKI:def 4, J1; :: thesis: verum

end;

then F2: M is Ideal of L by H0, FILTER_2:21;
F1: I c= M

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in I or t in M )
assume J1: t in I ; :: thesis: t in M
consider J being object such that
SS: J in Z by s1, XBOOLE_0:def 1;
J in { i where i is Ideal of L : ( I c= i & i misses F ) } by SS, s1;
then consider j being Ideal of L such that
SF: ( j = J & I c= j & j misses F ) ;
thus t in M by SS, TARSKI:def 4, J1, SF; :: thesis: verum

end;

M misses F

proof

assume M meets F ; :: thesis: contradiction
then consider x being object such that
F4: ( x in M & x in F ) by XBOOLE_0:3;
reconsider x = x as set by TARSKI:1;
consider y being set such that
F5: ( x in y & y in Z ) by TARSKI:def 4, F4;
y in { i where i is Ideal of L : ( I c= i & i misses F ) } by F5, s1;
then consider i being Ideal of L such that
F6: ( i = y & I c= i & i misses F ) ;
thus contradiction by F6, XBOOLE_0:3, F4, F5; :: thesis: verum

end;

hence union Z in { i where i is Ideal of L : ( I c= i & i misses F ) } by F1, F2; :: thesis: verum

end;

then consider Y being set such that
J0: ( Y in { i where i is Ideal of L : ( I c= i & i misses F ) } & ( for Z being set st Z in { i where i is Ideal of L : ( I c= i & i misses F ) } & Z <> Y holds
not Y c= Z ) ) by ORDERS_1:67, z1;
consider i being Ideal of L such that
KK: ( Y = i & I c= i & i misses F ) by J0;
take i ; :: thesis: ( i is prime & I c= i & i misses F )
i is prime

proof

assume not i is prime ; :: thesis: contradiction
then consider a, b being Element of L such that
G3: ( a "/\" b in i & not a in i & not b in i ) by Lem2;
set Ia = i "\/" (.a.>;
i c= i "\/" (.a.> by FILTER_2:50;
then J1: I c= i "\/" (.a.> by KK;
i "\/" (.a.> meets F

proof

assume i "\/" (.a.> misses F ; :: thesis: contradiction
then i "\/" (.a.> in { i where i is Ideal of L : ( I c= i & i misses F ) } by J1;
then UI: i "\/" (.a.> = i by FILTER_2:50, J0, KK;
(.a.> c= i "\/" (.a.> by FILTER_2:50;
hence contradiction by G3, UI, FILTER_2:28; :: thesis: verum

end;

then consider p1 being object such that
HH: ( p1 in i "\/" (.a.> & p1 in F ) by XBOOLE_0:3;
reconsider p1 = p1 as Element of L by HH;
consider p, q being Element of L such that
h1: ( p1 = p "\/" q & p in i & q in (.a.> ) by HH;
p "\/" q [= p "\/" a by FILTER_0:1, FILTER_2:28, h1;
then p "\/" a in F by FILTER_0:9, HH, h1;
then consider p being Element of L such that
G1: ( p in i & p "\/" a in F ) by h1;
set Ib = i "\/" (.b.>;
i c= i "\/" (.b.> by FILTER_2:50;
then J1: I c= i "\/" (.b.> by KK;
i "\/" (.b.> meets F

proof

assume i "\/" (.b.> misses F ; :: thesis: contradiction
then i "\/" (.b.> in { i where i is Ideal of L : ( I c= i & i misses F ) } by J1;
then UI: i "\/" (.b.> = i by FILTER_2:50, J0, KK;
(.b.> c= i "\/" (.b.> by FILTER_2:50;
hence contradiction by G3, UI, FILTER_2:28; :: thesis: verum

end;

then consider p1 being object such that
HH: ( p1 in i "\/" (.b.> & p1 in F ) by XBOOLE_0:3;
reconsider p1 = p1 as Element of L by HH;
consider P, Q being Element of L such that
h1: ( p1 = P "\/" Q & P in i & Q in (.b.> ) by HH;
P "\/" Q [= P "\/" b by FILTER_0:1, FILTER_2:28, h1;
then P "\/" b in F by FILTER_0:9, HH, h1;
then consider q being Element of L such that
G2: ( q in i & q "\/" b in F ) by h1;
set y = (p "\/" a) "/\" (q "\/" b);
Z1: (p "\/" a) "/\" (q "\/" b) in F by G1, G2, FILTER_0:8;
ZZ: (p "\/" a) "/\" (q "\/" b) = ((p "\/" a) "/\" q) "\/" ((p "\/" a) "/\" b) by LATTICES:def 11
.= ((p "/\" q) "\/" (a "/\" q)) "\/" ((p "\/" a) "/\" b) by LATTICES:def 11
.= ((p "/\" q) "\/" (a "/\" q)) "\/" ((p "/\" b) "\/" (a "/\" b)) by LATTICES:def 11
.= (((p "/\" q) "\/" (a "/\" q)) "\/" (p "/\" b)) "\/" (a "/\" b) by LATTICES:def 5
.= (((p "/\" q) "\/" (p "/\" b)) "\/" (a "/\" q)) "\/" (a "/\" b) by LATTICES:def 5 ;
set x = (((p "/\" q) "\/" (p "/\" b)) "\/" (a "/\" q)) "\/" (a "/\" b);
G4: p "/\" q in i by G2, FILTER_2:22;
G5: p "/\" b in i by G1, FILTER_2:22;
G6: a "/\" q in i by G2, FILTER_2:22;
(p "/\" q) "\/" (p "/\" b) in i by G4, G5, FILTER_2:21;
then ((p "/\" q) "\/" (p "/\" b)) "\/" (a "/\" q) in i by G6, FILTER_2:21;
then (((p "/\" q) "\/" (p "/\" b)) "\/" (a "/\" q)) "\/" (a "/\" b) in i by FILTER_2:21, G3;
hence contradiction by KK, XBOOLE_0:3, Z1, ZZ; :: thesis: verum

end;

hence ( i is prime & I c= i & i misses F ) by KK; :: thesis: verum