let L be distributive Lattice; :: thesis: for I being Ideal of L
for a being Element of L st not a in I holds
ex P being Ideal of L st
( P is prime & I c= P & not a in P )
let I be Ideal of L; :: thesis: for a being Element of L st not a in I holds
ex P being Ideal of L st
( P is prime & I c= P & not a in P )
let a be Element of L; :: thesis: ( not a in I implies ex P being Ideal of L st
( P is prime & I c= P & not a in P ) )
assume A0: not a in I ; :: thesis: ex P being Ideal of L st
( P is prime & I c= P & not a in P )
set F = <.a.);
A2: a in <.a.) ;
I misses <.a.)

proof

assume I meets <.a.) ; :: thesis: contradiction
then consider x being object such that
A1: ( x in I & x in <.a.) ) by XBOOLE_0:3;
reconsider x = x as Element of L by A1;
a [= x by A1, FILTER_0:15;
hence contradiction by A0, FILTER_2:21, A1; :: thesis: verum

end;

then consider P being Ideal of L such that
T1: ( P is prime & I c= P & P misses <.a.) ) by Th15;
not a in P by A2, T1, XBOOLE_0:3;
hence ex P being Ideal of L st
( P is prime & I c= P & not a in P ) by T1; :: thesis: verum