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 :: thesis: for a being object st a in I holds
not a in uparrow x

let a be object ; :: thesis: ( a in I implies not a in uparrow x )
assume that
A2: a in I and
A3: a in uparrow x ; :: thesis: contradiction
reconsider a = a as Element of L by A2;
a >= x by A3, 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
A4: ( P is prime & I c= P ) and
A5: P misses uparrow x by Th23;
take P ; :: thesis: ( P is prime & I c= P & not x in P )
thus ( P is prime & I c= P ) by A4; :: thesis: not x in P
assume x in P ; :: thesis: contradiction
then not x in uparrow x by A5, XBOOLE_0:3;
then not x <= x by WAYBEL_0:18;
hence contradiction ; :: thesis: verum