let L be distributive LATTICE; :: thesis: for I being Ideal of L
for x being Element of L st not x in I holds
ex P being Ideal of L st
( P is prime & I c= P & not x in P )
let I be Ideal of L; :: thesis: for x being Element of L st not x in I holds
ex P being Ideal of L st
( P is prime & I c= P & not x in P )
let x be Element of L; :: thesis: ( not x in I implies ex P being Ideal of L st
( P is prime & I c= P & not x in P ) )
assume A1: not x in I ; :: thesis: ex P being Ideal of L st
( P is prime & I c= P & not x in P )

now

let a be set ; :: thesis: ( a in I implies not a in uparrow x )
assume A2: ( a in I & a in uparrow x ) ; :: thesis: contradiction
then reconsider a = a as Element of L ;
a >= x by A2, WAYBEL_0:18;
hence contradiction by A1, A2, WAYBEL_0:def 19; :: thesis: verum

end;

then I misses uparrow x by XBOOLE_0:3;
then consider P being Ideal of L such that
A3: ( P is prime & I c= P & P misses uparrow x ) by Th27;
take P ; :: thesis: ( P is prime & I c= P & not x in P )
thus ( P is prime & I c= P ) by A3; :: thesis: not x in P
assume x in P ; :: thesis: contradiction
then not x in uparrow x by A3, XBOOLE_0:3;
then not x <= x by WAYBEL_0:18;
hence contradiction ; :: thesis: verum